package com.example.heraclitoapp;

/** lastbtn
 * 1. Modus Ponens
 * 2. Adicao
 * 3. CJ
 * 4. Inclusao da Equivalencia - IEQ 
 * 5. Eliminacao da Equivalencia -EQ
 * 6. SP
 * 7. Eliminacao da Disjuncao - -EDJ
 * 8. PC
 * 9. RAA
 * 10. DN
 * 11. Modus Tollens
 * 12. SH
 * 13. SD 
 * 14. INC
 * 15. Dilema Construtivo - DC
 * 16. EXP
 */

//import android.R;
import heraclito.Linha;
import heraclito.Teorema;

import java.io.BufferedReader;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileOutputStream;
import java.io.FileWriter;
import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.io.ObjectInputStream;
import java.io.ObjectOutputStream;
import java.io.PrintWriter;
import java.util.ArrayList;
import java.util.Calendar;
import java.util.List;
import java.util.Timer;
import java.util.TimerTask;
import java.util.concurrent.ExecutionException;
import java.util.concurrent.Future;
//import java.util.concurrent.ExecutionException;
//import java.util.logging.Level;
//import java.util.logging.Logger;































import org.ksoap2.HeaderProperty;
import org.ksoap2.SoapEnvelope;
//import org.ksoap2.SoapFault;
//import org.ksoap2.serialization.KvmSerializable;
import org.ksoap2.serialization.PropertyInfo;
import org.ksoap2.serialization.SoapObject;
import org.ksoap2.serialization.SoapPrimitive;
import org.ksoap2.serialization.SoapSerializationEnvelope;
import org.ksoap2.transport.HttpTransportSE;
import org.xmlpull.v1.XmlPullParserException;









//import com.WSParser.WebServices.WSAgentService.*;
//import android.annotation.TargetApi;
import android.app.Activity;
import android.app.AlertDialog;
import android.app.AlertDialog.Builder;
import android.app.Dialog;
//import android.net.http.AndroidHttpClient;
import android.os.AsyncTask;
import android.os.Bundle;
import android.os.Handler;
import android.renderscript.Element;
//import android.os.StrictMode;
//import android.os.SystemClock;
//import android.test.PerformanceTestCase;
import android.util.Log;
import android.view.*;
import android.view.animation.AlphaAnimation;
import android.view.animation.Animation;
import android.view.animation.AnimationUtils;
import android.webkit.WebSettings.ZoomDensity;
import android.webkit.WebView;
import android.widget.*;
//import android.widget.ViewSwitcher.ViewFactory;
import android.app.*;
import android.content.Context;
import android.content.DialogInterface;
import android.content.Intent;
import logic.Formula;
import logic.ParserException;
import logic.ScannerException;
import android.graphics.PorterDuff;
import android.graphics.Color;
import android.graphics.PorterDuffColorFilter;
import android.graphics.drawable.Drawable;
import android.widget.TabHost;

/**
 *  TODO
 
 	RAA antes das hipoteses nao pode
    Registrar .her com aplicativo
    AgentCommList
    Icone
    Depois de carregar, resolucao = null? - WEIRD
    Setar para null resolução - WEIRD
    Ao errar linha de regra, exibir Toast
    scrollist
    
    On Progress
   
   	Regras
   
    DONE
    
    Nova aba
    Fechar aba
    Carregar e Salvar Prova (FALTAR TESTAR TABLET - suponho que works)
    Pacotes com Teorema e Linha tem que estar mesmo que o desktop para ser possível salvar
    NÃO PODE SER STATIC - dar compare to -> each other
    Logoff
    TabActivity -> MainActivity, LoginDialog
    Botão Login só nas provas
    Ajustar permissões no android manifest
    Exemplos
    Resolução Provador
    Escrever argumento [revisar spinners]
   	Revisar o iniciar()
    habilitaBotoesInterface()
   
    ----------------------------------------------------------------------------------------------------
    
    TestaRegra() nas seguintes regras:
    
    MP
    CJ
    AD
    DJ
    IEQ
    DN
    SP
    menosEQ
    MT
    SD
    SH
    DC
    EXP
    INC
 */

public class HeraclitoActivity extends Activity {
	/** Called when the activity is first created. */

	public final int PROPOSITION = 1, PARENTHESIS = 2, NEGATION = 3,
			CONJUNCTION = 4, DISJUNCTION = 5, CONDITIONAL = 6,
			BICONDITIONAL = 7;
	protected int opcao = 0;
	protected boolean carregar = false;
	protected int lastbtn = 0; // ultima regra
	protected int pos1 = 0; // Variaveis que controlam a seleção das opções
							// para as regras
	protected int pos2 = 0; // Variaveis que controlam a seleção das opções
							// para as regras
	protected int pos3 = 0; // Variaveis que controlam a seleção das opções
							// para as regras
	protected Linha Teorema[]; // Teorema original
	protected Linha TeoremaAux[]; // Teorema auxiliar que controla
									// Desfazer/Refazer
	//protected Linha hipoteses[];
	protected Formula hipoteses[];

	protected int indiceoriginal = 0; // Tamanho máximo do teorema
	protected int indice = 0; // Controla a posição do teorema no Desfazer e
								// Refazer
	protected int total_hipoteses = 0;// Variavel que controla a ação de
										// desfazer
	protected int qtPCRAA = 0;// indica quantos '|' colocar
	protected String resPCRAA[];// indica qual a fórmula a ser derivada das
								// regras PC e RAA, e também qual das duas
								// regras foi a ultima utilizada

	private ListView teoremalist;
	private ListView agentCommList;
	private Spinner sp1;
	private int ultimoBotao;
	private SelectedAdapter selectedAdapter;
	private SelectedAdapterAgent selectedAdapterAgent;
	private ArrayList<String> msgAgent = new ArrayList<String>();
	private String[] resolucao;
	private String nivel; //TODO
	private String argumentoFormatado;
	private int qtAjuda;
	private int qtErrosRegras[];
	private int qtErrosSeguidos[];
	private boolean regraCorreta = false;
	private Spinner sp2_selecionar;
	private int tabCount;
	private View separador;	
	private SelectedAdapter selectedAdapterProvador;
	private ListView provadorlist;	
	private EditText adicionar_argumento;
	Button btn_adicionaHip;
	
	// Alterna entre o modo de apenas escrever o argumento
	public final boolean ADICIONAR_ARGUMENTO = false;
	
	private static final String regras[] = {"MP","AD","CJ","IEQ","EEQ","SP","EDJ","PC","RAA",
	        "DN","MT","SH","SD","INC","DC","EXP"};

	//ksoap2
	//performLogin2Response
	private static final String METHOD_NAME = "performLogin2"; //ws chamado TODO
	private static final String METHOD_NAME2 = "sendMessageToAgent";
	//The name of the web service operation, which may be obtained form the WSDL.
	private static final String NAMESPACE = "http://ws.org.br/"; //ws caminho
	//Namespace is the targetNamespace in the WSDL.
	private static final String URL = "http://obaa.unisinos.br:80/WSServer/WSAgent?wsdl"; //service .xml WSDL
	
	/** URL: The WSDL URL. Its value is the location attribute of the soap:address element 
	for a port element in a WSDL. Unless the web service is also hosted on the Android device,
	the hostname should not be specified as localhost, because the application runs on the Android
	device while the web service is hosted on the localhost server. 
	Specify hostname as the IP address of the server hosting the web service. **/
	
	private static final String SOAP_ACTION = NAMESPACE + METHOD_NAME;
	private static final String SOAP_ACTION2 = NAMESPACE + METHOD_NAME2;
	
	SoapObject request = new SoapObject(NAMESPACE, METHOD_NAME);
	SoapObject request2 = new SoapObject(NAMESPACE, METHOD_NAME2);
	
	PropertyInfo pi = new PropertyInfo(); //dado mandado para o ws
	
	PropertyInfo userId = new PropertyInfo();
	PropertyInfo password = new PropertyInfo();
	PropertyInfo localHost = new PropertyInfo();
	
	
	
	//String usuario;
	//String senha;
	
	@Override
	public void onCreate(Bundle savedInstanceState) {
		super.onCreate(savedInstanceState);
		setContentView(R.layout.main);
		
		
		btn_adicionaHip = (Button) findViewById(R.id.adicionarHip);
		/**
		if (android.os.Build.VERSION.SDK_INT > 9) {
        	StrictMode.ThreadPolicy policy = new StrictMode.ThreadPolicy.Builder().permitAll().build();
            StrictMode.setThreadPolicy(policy);
		}**/
		
		/**
		final Dialog login_dialog = new Dialog(HeraclitoActivity.this);
		login_dialog.setTitle("Login");
		login_dialog.setContentView(R.layout.login);

		final Button login_ok = (Button) login_dialog.findViewById(R.id.login_ok);
		final Button login_cancelar = (Button) login_dialog.findViewById(R.id.login_cancelar);

		final EditText login_caixa = (EditText) login_dialog.findViewById(R.id.login_caixa);
		final EditText login_password = (EditText) login_dialog.findViewById(R.id.login_password);
		
		final ProgressBar progress = (ProgressBar) login_dialog.findViewById(R.id.progressBar1);
		final TextSwitcher mensagemLogin = (TextSwitcher) login_dialog.findViewById(R.id.mensagemLogin);

		final TextView mensagemLogadoComo = (TextView) findViewById(R.id.logadoComo);
		
		
		login_ok.setOnClickListener(new View.OnClickListener() {
			
			public void onClick(View v) {	
				MainActivity.usuario = login_caixa.getText().toString();
				MainActivity.senha = login_password.getText().toString();
				
				Animation in = AnimationUtils.loadAnimation(getBaseContext(), android.R.anim.fade_in);
				Animation out = AnimationUtils.loadAnimation(getBaseContext(), android.R.anim.fade_out);
		
				mensagemLogin.setInAnimation(in);
				mensagemLogin.setOutAnimation(out);
				
				
				
				if (mensagemLogin.getChildCount() > 0) {
					mensagemLogin.removeAllViews();
				}
				
				mensagemLogin.addView(new TextView(getBaseContext()));
				mensagemLogin.addView(new TextView(getBaseContext()));
				
				
				new Login(getBaseContext(), progress, login_dialog, mensagemLogin, mensagemLogadoComo).execute(MainActivity.usuario, MainActivity.senha);
				//telaLogin.execute(usuario, senha);
				
				
				
				
				
								/**
				TextView ra = (TextView) findViewById(R.id.debug);
				
				if (resposta == null) {
					ra.setText("nulo");
				} else {
					login_dialog.dismiss();
					ra.setText(resposta);
					
				}
				//login_dialog.dismiss();
			}
		});
		
		login_cancelar.setOnClickListener(new View.OnClickListener() {
			
			public void onClick(View v) {
			
				login_dialog.dismiss();
			}
		});
		
		login_dialog.show();*/
		
		//ksoap2
		//pi.setName("teste"); //nome da variavel que sera passada
		//pi.setValue(value); //variavel enviada para ws, retorna resultado
		//pi.setType(type); //tipo da variavel, pode ser qualquer object
		//request.addProperty(pi); //adiciona ao objeto request
		
		//method hello
		//pi.name="arg0";
		//pi.type=PropertyInfo.STRING_CLASS;
		//request.addProperty(pi, "Adam"); //adiciona ao objeto request
		
		//recebe o objeto do ws, e entrega de volta a app
		//SoapSerializationEnvelope envelope = new SoapSerializationEnvelope(SoapEnvelope.VER11);
		//define o objeto de retorno, nao obrigatorio (devolve object)
		//envelope.addMapping(NAMESPACE, nomeObjetoRetorno, Object.class);
		//manda esse objeto e recebe outro
		//envelope.setOutputSoapObject(request);
		
		
		Teorema = new Linha[100];
		resPCRAA = new String[50];

		// criacao de todos botoes
		sp1 = (Spinner) findViewById(R.id.spinner1);
		sp2_selecionar = (Spinner) findViewById(R.id.spinner_selecionar);
		
		final Button btn_provar = (Button) findViewById(R.id.btn_provar);
		final Button btn_ajuda = (Button) findViewById(R.id.btn_ajuda);
		
		teoremalist = (ListView) findViewById(R.id.teoremalist);
		agentCommList = (ListView) findViewById(R.id.agenteCommList);
		
		separador = (View) findViewById(R.id.separator);
		
		provadorlist = (ListView) findViewById(R.id.provadorlist);
		
		final TextView selecione_argumento = (TextView) findViewById(R.id.textView1);
		adicionar_argumento = (EditText) findViewById(R.id.editText1);
		
		
		ArrayList<String> exercicios = new ArrayList<String>();
		
		
		if (ADICIONAR_ARGUMENTO) {
			sp1.setVisibility(View.INVISIBLE);
			sp2_selecionar.setVisibility(View.INVISIBLE);
			adicionar_argumento.setVisibility(View.VISIBLE);
		} else {
			exercicios.add(getString(R.string.nivel_basico));
			exercicios.add(getString(R.string.nivel_intermediario));
			exercicios.add(getString(R.string.nivel_avancado));
			exercicios.add(getString(R.string.nivel_exercicios));
		}
			exercicios.add(getString(R.string.nivel_argumento));
				

		//	exercicios.add("Adicionar argumento");
		
		 
		
		/**
		ArrayList<String> exercicios = new ArrayList<String>();
		exercicios.add("Basico");
		exercicios.add("Intermediario");
		exercicios.add("Avancado");
		exercicios.add("Lista_de_exercicio");*/
		
		sp2_selecionar.setAdapter(new ArrayAdapter<String>(HeraclitoActivity.this,
				android.R.layout.simple_list_item_1, exercicios));
		
		//sp1.setAdapter(new ArrayAdapter<String>(HeraclitoActivity.this,
			//	android.R.layout.simple_list_item_1, exercicios));
		
		sp2_selecionar
		.setOnItemSelectedListener(new AdapterView.OnItemSelectedListener() {

			public void onItemSelected(AdapterView<?> parent,
					View view, int pos, long id) {
				// An spinnerItem was selected. You can retrieve the
				// selected item using
				// parent.getItemAtPosition(pos)
				nivel = sp2_selecionar.getSelectedItem().toString();
				
				if (nivel.equals(getString(R.string.nivel_argumento))) {
					sp1.setVisibility(View.INVISIBLE);
					adicionar_argumento.setVisibility(View.VISIBLE);
					selecione_argumento.setText(getString(R.string.digite_o_argumento));
					//sp2_selecionar.setRight(R.id.textView1);
				} else {
					sp1.setVisibility(View.VISIBLE);
					sp2_selecionar.setRight(R.id.spinner1);
					adicionar_argumento.setVisibility(View.INVISIBLE);
					if (nivel.equals(getString(R.string.nivel_exercicios))) { //TODO GAMBIARRA WORKAROUND
						selecione_argumento.setText("Selec..");
					} else {
						selecione_argumento.setText(getString(R.string.argumento));
					}
					leArquivoArgumentos();
				}
			
			}

			public void onNothingSelected(AdapterView<?> parent) {
				// Do nothing, just another required interface callback
			}
		});

		
		//leArquivoArgumentos();
		/**
		InputStream argumentos = getResources().openRawResource(
				R.raw.argumentos);
		InputStreamReader isr = new InputStreamReader(argumentos);

		BufferedReader bf = new BufferedReader(isr);

		ArrayList<String> lista = new ArrayList<String>();
		try {
			lista.add(bf.readLine());
			while (lista.get(lista.size() - 1) != null) {
				lista.add(bf.readLine());
			}
			bf.close();
		} catch (IOException e) {
			// 
			e.printStackTrace();
		}

		lista.remove(lista.size() - 1);

		sp1.setAdapter(new ArrayAdapter<String>(HeraclitoActivity.this,
				android.R.layout.simple_list_item_1, lista));**/

		//String[] teste2 = {"lucas", "marcel"};
	
		
		teoremalist
				.setOnItemClickListener(new AdapterView.OnItemClickListener() {
					
					public void onItemClick(AdapterView<?> arg0, View arg1,
							int position, long id) {
						
						if (!Teorema[position].isUsable()) {
							Toast t = Toast.makeText(getBaseContext(), getString(R.string.linha_inutilizavel), Toast.LENGTH_SHORT); 
							t.setGravity(Gravity.TOP, 0, 100+(int)arg1.getY());
							t.show();
						} else if (carregar) {
							// Seta posi�ao
							if (pos1 == 0 && pos2 != position) {
								pos1 = position;
								if (pos1 <= indice) {
									if (lastbtn == 5) {
										Regra_menosEQ();
									} else if (lastbtn == 2) {
										dialogo_AD();
									} else if (lastbtn == 6) {
										Regra_SP();
									} else if (lastbtn == 10) {
										Regra_DN();
									} else if (lastbtn == 16) {
										// Regra_EXP();
									} else {
										// arg1.setBackgroundColor(Color.CYAN);
										selectedAdapter
												.setSelectedPosition1(position);
									}
								} else {
									pos1 = 0;
								}
							} else if (pos1 == position) {
								// arg1.setBackgroundColor(Color.TRANSPARENT);
								selectedAdapter.setSelectedPosition1(0);
								pos1 = 0;
							} else if (pos2 == 0) {
								pos2 = position;
								if (pos2 <= indice) {
									if (lastbtn == 1) {
										Regra_MP();
									} else if (lastbtn == 3) {
										Regra_CJ();
									} else if (lastbtn == 4) {
										Regra_IEQ();
									} else if (lastbtn == 11) {
										Regra_MT();
									} else if (lastbtn == 12) {
										Regra_SH();
									} else if (lastbtn == 13) {
										Regra_SD();
									} else if (lastbtn == 14) {
										Regra_INC();
									} else {
									// arg1.setBackgroundColor(Color.CYAN);
										selectedAdapter
												.setSelectedPosition2(position);
									}
								} else {
									pos2 = 0;
								}
							} else if (pos2 == position) {
								// arg1.setBackgroundColor(Color.TRANSPARENT);
								selectedAdapter.setSelectedPosition2(0);
								pos2 = 0;
							} else if (pos3 == 0) {
								pos3 = position;
								if (pos3 <= indice) {
									if (lastbtn == 7) {
										Regra_DJ();
									} else if (lastbtn == 15) {
										Regra_DC();
									}
								} else {
									pos3 = 0;
								}
							}
						}
					}
				});

		btn_provar.setOnClickListener(new View.OnClickListener() {

			public void onClick(View v) {
				
				Iniciar();
			}
		});
		
		/**
		sp1.setOnItemSelectedListener(new AdapterView.OnItemSelectedListener() {
			
			public void onItemSelected(AdapterView<?> parent, View view, 
                    int pos, long id) {
                // An spinnerItem was selected. You can retrieve the selected item using
                // parent.getItemAtPosition(pos)
				Iniciar();
            }

            public void onNothingSelected(AdapterView<?> parent) {
                // Do nothing, just another required interface callback
            }
		});**/

		
				
		/*
		sp2_selecionar.setOnItemSelectedListener(new AdapterView.OnItemSelectedListener() {
			
			public void onItemSelected(AdapterView<?> parent, View view, 
                    int pos, long id) {
                // An spinnerItem was selected. You can retrieve the selected item using
                // parent.getItemAtPosition(pos)
				leArquivoArgumentos();
            }

            public void onNothingSelected(AdapterView<?> parent) {
                // Do nothing, just another required interface callback
            }
		});*/
		
		/**
		btn_selecionar.setOnClickListener(new View.OnClickListener() {
			
			public void onClick(View arg0) {
				leArquivoArgumentos();
			}
		});**/
		// Botao RAA
		btn_adicionaHip.setOnClickListener(new View.OnClickListener() {
			
			public void onClick(View v) {
				if (Teorema[0] == null) {
					Toast.makeText(HeraclitoActivity.this, getString(R.string.aperte_provar),
					Toast.LENGTH_LONG).show();
					return;
				}
				alteraCor();
				final Dialog d = new Dialog(HeraclitoActivity.this);
				d.setContentView(R.layout.dialogo_hip);
				d.setTitle(R.string.mensagem);
				
				Button ok = (Button) d.findViewById(R.id.dialogoHip_ok);
				Button bcan = (Button) d.findViewById(R.id.dialogoHip_cancel);
				final EditText caixa = (EditText) d
						.findViewById(R.id.dialogo_inputHip);
				//TextView tv = (TextView) d.findViewById(R.id.textView1);
				//tv.setText("Digite a f�rmula que deseja negar usando a regra RAA.\n"
				//		+ "Por exemplo: a para provar ~a.");

				final TextSwitcher mensagemHip = (TextSwitcher) d.findViewById(R.id.dialogoHip_textoErro);
				
				Animation in = AnimationUtils.loadAnimation(getBaseContext(), android.R.anim.fade_in);
				Animation out = AnimationUtils.loadAnimation(getBaseContext(), android.R.anim.fade_out);
		
				mensagemHip.setInAnimation(in);
				mensagemHip.setOutAnimation(out);
				
				if (mensagemHip.getChildCount() > 0) {
					mensagemHip.removeAllViews();
				}
				
				mensagemHip.addView(new TextView(getBaseContext()));
				mensagemHip.addView(new TextView(getBaseContext()));
				
				TextView adicionaHipTexto = (TextView) mensagemHip.getChildAt(0);
				adicionaHipTexto.setTextColor(Color.BLACK);
							
				TextView adicionaHipTexto2 = (TextView) mensagemHip.getChildAt(1);
				adicionaHipTexto2.setTextColor(Color.BLACK);
				
				ok.setOnClickListener(new View.OnClickListener() {

					public void onClick(View v) {
						
						String temp = caixa.getText().toString();
						if (!temp.equalsIgnoreCase(""))
							adicionaHip(temp, mensagemHip);
						d.dismiss();
					}
				});

				bcan.setOnClickListener(new View.OnClickListener() {

					public void onClick(View v) {
						

						d.dismiss();
					}
				});

				d.show();
			}
		});
				
		btn_ajuda.setOnClickListener(new View.OnClickListener() {
			
			public void onClick(View v) {
				final Dialog d = new Dialog(HeraclitoActivity.this);
				d.setContentView(R.layout.dialogo_ajuda);
				d.setTitle(R.string.mensagem);
				
				final RadioGroup rg = (RadioGroup) d.findViewById(R.id.radioGroup1);
				
				Button btn_ok = (Button) d.findViewById(R.id.btn_SPok);
				Button btn_cancel = (Button) d.findViewById(R.id.btn_cancel);
				
				btn_ok.setOnClickListener(new View.OnClickListener() {
				
					public void onClick(View v) {
						
						tabCount = MainActivity.tabHost.getTabWidget().getTabCount();
						
						
						switch (rg.getCheckedRadioButtonId()) {
							case R.id.radio0:
								
								//String manual = getString(R.string.manual);
								
								MainActivity.tabHost.getTabWidget().getChildTabViewAt(1).setVisibility(View.VISIBLE);
								MainActivity.tabHost.setCurrentTab(1);
								
								/**
								for (int i = 0; i < tabCount; i++) {
									if (MainActivity.tabHost.getTabWidget().getChildTabViewAt(i).getTag().toString().equals(manual)) {
										//TabActivity.tabHost.setCurrentTab(i);
										MainActivity.tabHost.getTabWidget().getChildTabViewAt(i).setVisibility(View.VISIBLE);
										MainActivity.tabHost.setCurrentTabByTag(manual);
										d.dismiss();
										return;
									}
								}**/
								
								
								
								break;
								/**
								int tabAtual = ++MainActivity.prova; //DELETAR
								Intent intentManual = new Intent().setClass(getApplicationContext(), Manual.class);
								TabHost.TabSpec specManual = MainActivity.tabHost.newTabSpec(String.valueOf(tabAtual)).setIndicator("Manual").setContent(intentManual);
								MainActivity.tabHost.addTab(specManual);
								
								MainActivity.tabHost.setCurrentTab(tabAtual);
								/**
								final Dialog manual_dialog = new Dialog(HeraclitoActivity.this);
								manual_dialog.setTitle("Manual");
								manual_dialog.setContentView(R.layout.dialogo_manual);
								WebView manual = (WebView) manual_dialog.findViewById(R.id.webview);
								manual.getSettings().setBuiltInZoomControls(true);
								manual.getSettings().setDefaultZoom(ZoomDensity.FAR);;
								manual.loadUrl("file:///android_asset/manual/Manual_do_Heraclito.htm");
								manual_dialog.show();**/
								
							case R.id.radio1:
								//TODO Exemplos
								//if (qtAjuda < 1) {
								//	qtAjuda = 1;
								//}
								SelecaoExemplos(d);
								break;
							case R.id.radio2:
								if (qtAjuda == 0) {
										SelecaoExemplos(d); 
						            } else {
						                if (indice < total_hipoteses) {
						                    String msg = getString(R.string.proxima_hipotese) + hipoteses[0].display();
						                    escreveParaUsuario(msg);
						                } else {
						                    comunicaServidor("solic_ajuda", "ajuda solicitada");
						                }
						            }
						            ++qtAjuda;
						            break;
						}
						
						
						d.dismiss();
					}
				});
				
				btn_cancel.setOnClickListener(new View.OnClickListener() {
					
					public void onClick(View v) {
						
						d.dismiss();
					}
				});
				
				d.show();
				
			}
		});
	}
	
	public void SelecaoExemplos(Dialog d) {
		
		MainActivity.tabHost.getTabWidget().getChildTabViewAt(2).setVisibility(View.VISIBLE);
		MainActivity.tabHost.setCurrentTab(2);
		/**
		
		String exemplo = getString(R.string.exemplos);
		boolean abaEncontrada = false;
		
		for (int i = 0; i < tabCount ; i++) {
			if (MainActivity.tabHost.getTabWidget().getChildTabViewAt(i).getTag().toString().equals(exemplo)) {
				//TabActivity.tabHost.setCurrentTab(i);
				
				MainActivity.tabHost.getTabWidget().getChildTabViewAt(i).setVisibility(View.VISIBLE);
				MainActivity.tabHost.setCurrentTabByTag(exemplo);
				d.dismiss();
				abaEncontrada = true;
				return;
			} 
		}
		
		if (!abaEncontrada) {
			Intent intentExemplos = new Intent().setClass(getApplicationContext(), ExemplosActivity.class);
			TabHost.TabSpec specExemplos = MainActivity.tabHost.newTabSpec(exemplo).setIndicator(exemplo).setContent(intentExemplos);
			MainActivity.tabHost.addTab(specExemplos);
			MainActivity.tabHost.getTabWidget().getChildTabViewAt(tabCount).setTag(exemplo);
			MainActivity.tabHost.setCurrentTabByTag(exemplo);
		} **/
		
		if (qtAjuda < 1) {
			qtAjuda = 1;
		}
		
	}
	
	
	
	public void habilitaBotoesInterface() {
		
		if (Teorema[0] != null) {
			
			final Button btn_RAA = (Button) findViewById(R.id.btn_RAA);
			final Button btn_DN = (Button) findViewById(R.id.btn_DN);
			final Button btn_PC = (Button) findViewById(R.id.btn_PC);
			final Button btn_MP = (Button) findViewById(R.id.btn_MP);

			final Button btn_CJ = (Button) findViewById(R.id.btn_CJ);
			final Button btn_SP = (Button) findViewById(R.id.btn_SP);
			final Button btn_AD = (Button) findViewById(R.id.btn_AD);
			final Button btn_DJ = (Button) findViewById(R.id.btn_DJ);

			final Button btn_maisEQ = (Button) findViewById(R.id.btn_maisEQ);
			final Button btn_menosEQ = (Button) findViewById(R.id.btn_menosEQ);

			final Button btn_MT = (Button) findViewById(R.id.btn_MT);
			final Button btn_SH = (Button) findViewById(R.id.btn_SH);
			final Button btn_SD = (Button) findViewById(R.id.btn_SD);
			final Button btn_DC = (Button) findViewById(R.id.btn_DC);

			final Button btn_EXP = (Button) findViewById(R.id.btn_EXP);
			final Button btn_INC = (Button) findViewById(R.id.btn_INC);
			
			final Button btn_desfazer = (Button) findViewById(R.id.desfazer);
			final Button btn_refazer = (Button) findViewById(R.id.refazer);
			

			btn_RAA.setOnClickListener(new View.OnClickListener() {

				public void onClick(View v) {
					
					alteraCor();
					final Dialog d = new Dialog(HeraclitoActivity.this);
					d.setContentView(R.layout.dialogo);
					d.setTitle(R.string.mensagem);

					Button ok = (Button) d.findViewById(R.id.btok);
					Button bcan = (Button) d.findViewById(R.id.bcancel);
					final EditText caixa = (EditText) d
							.findViewById(R.id.dialogocaixa);
					//TextView tv = (TextView) d.findViewById(R.id.textView1);
					//tv.setText("Digite a f�rmula que deseja negar usando a regra RAA.\n"
					//		+ "Por exemplo: a para provar ~a.");				
					
					ok.setOnClickListener(new View.OnClickListener() {

						public void onClick(View v) {
							
							String temp = caixa.getText().toString();
							if (!temp.equalsIgnoreCase(""))
								Regra_RAA(temp);
							d.dismiss();
						}
					});

					bcan.setOnClickListener(new View.OnClickListener() {

						public void onClick(View v) {
							

							d.dismiss();
						}
					});

					d.show();
				}
			});

			btn_PC.setOnClickListener(new View.OnClickListener() {

				public void onClick(View v) {
					
					alteraCor();
					final Dialog d = new Dialog(HeraclitoActivity.this);
					d.setContentView(R.layout.dialogo);
					d.setTitle(R.string.mensagem);
					
					Button ok = (Button) d.findViewById(R.id.btok);
					Button bcan = (Button) d.findViewById(R.id.bcancel);
					final EditText caixa = (EditText) d
							.findViewById(R.id.dialogocaixa);
					TextView tv = (TextView) d.findViewById(R.id.textView1);
					tv.setText(getString(R.string.formula_pc) + "\n" + getString(R.string.formula_pc_exemplo));

					ok.setOnClickListener(new View.OnClickListener() {

						public void onClick(View v) {
							
							String temp = caixa.getText().toString();
							if (!temp.equalsIgnoreCase(""))
								Regra_PC(temp);
							d.dismiss();
						}
					});

					bcan.setOnClickListener(new View.OnClickListener() {

						public void onClick(View v) {
							

							d.dismiss();
						}
					});

					d.show();
				}
			});

			btn_MP.setOnClickListener(new View.OnClickListener() {

				public void onClick(View v) {
					
					alteraCor();
					ultimoBotao = btn_MP.getId();
					Regra_MP();

				}
			});

			btn_AD.setOnClickListener(new View.OnClickListener() {

				public void onClick(View v) {
					
					alteraCor();
					ultimoBotao = btn_AD.getId();
					Regra_AD();

				}
			});

			btn_DJ.setOnClickListener(new View.OnClickListener() {

				public void onClick(View v) {
					
					alteraCor();
					ultimoBotao = btn_DJ.getId();
					Regra_DJ();
				}

			});

			btn_CJ.setOnClickListener(new View.OnClickListener() {

				public void onClick(View v) {
					
					alteraCor();
					ultimoBotao = btn_CJ.getId();
					Regra_CJ();
				}

			});

			btn_maisEQ.setOnClickListener(new View.OnClickListener() {

				public void onClick(View v) {
					
					alteraCor();
					ultimoBotao = btn_maisEQ.getId();
					Regra_IEQ();
				}

			});

			btn_DN.setOnClickListener(new View.OnClickListener() {

				public void onClick(View v) {
					
					alteraCor();
					ultimoBotao = btn_DN.getId();
					Regra_DN();
				}

			});

			btn_SP.setOnClickListener(new View.OnClickListener() {

				public void onClick(View v) {
					
					alteraCor();
					ultimoBotao = btn_SP.getId();
					Regra_SP();
				}

			});

			btn_menosEQ.setOnClickListener(new View.OnClickListener() {

				public void onClick(View v) {
					
					alteraCor();
					ultimoBotao = btn_menosEQ.getId();
					Regra_menosEQ();
				}
			});

			btn_MT.setOnClickListener(new View.OnClickListener() {

				public void onClick(View v) {
					
					alteraCor();
					ultimoBotao = btn_MT.getId();
					Regra_MT();
				}

			});

			btn_SH.setOnClickListener(new View.OnClickListener() {

				public void onClick(View v) {
					
					alteraCor();
					ultimoBotao = btn_SH.getId();
					Regra_SH();
				}

			});

			btn_SD.setOnClickListener(new View.OnClickListener() {

				public void onClick(View v) {
					
					alteraCor();
					ultimoBotao = btn_SD.getId();
					Regra_SD();
				}

			});

			btn_DC.setOnClickListener(new View.OnClickListener() {

				public void onClick(View v) {
					
					alteraCor();
					ultimoBotao = btn_DC.getId();
					Regra_DC();
				}

			});

			btn_EXP.setOnClickListener(new View.OnClickListener() {

				public void onClick(View v) {
					
					alteraCor();
					ultimoBotao = btn_EXP.getId();
					Regra_EXP();
				}

			});

			btn_INC.setOnClickListener(new View.OnClickListener() {

				public void onClick(View v) {
					
					alteraCor();
					ultimoBotao = btn_INC.getId();
					Regra_INC();
				}

			});
			
			btn_desfazer.setOnClickListener(new View.OnClickListener() {
				
				public void onClick(View v) {
					alteraCor();
					desfazer();
				}
			});
			
			btn_refazer.setOnClickListener(new View.OnClickListener() {
				
				public void onClick(View v) {
					alteraCor();
					refazer();
				}
			});

			
		}
		
	}
		
	public void Regra_RAA(String formula) {
		/*
		 * if (!carregar || lastbtn != 9) { carregar = true;
		 * Teorema[pos1].unselect(); Teorema[pos2].unselect(); lastbtn = 9; }
		 * else {
		 */
		try {
			// Atualiza variaveis de controle
			carregar = false;
			++qtPCRAA;
			Formula f = new Formula();
			f.parse(formula);
			f = this.eliminaParenteses(f, true);
			Teorema[++indice] = new Linha(f, " ", "HIP-RAA ", qtPCRAA, indice);
			resPCRAA[qtPCRAA - 1] = formula;
			resPCRAA[50 - qtPCRAA] = "raa";

			ajusta();

			organiza();
			
			comunicaServidor("diag_prova", "regra aplicada");

		} catch (ScannerException ex) {
			// JOptionPane.showMessageDialog(null, "Erro na f�rmula.");
		} catch (ParserException ex) {
			// JOptionPane.showMessageDialog(null, "Erro na f�rmula.");
		}
	}

	// }

	public void Regra_MP() {
		// Executa a ação do usuário

		if (!carregar || lastbtn != 1) {
			// Altera cor do bot�o
			Drawable d = findViewById(R.id.btn_MP).getBackground();
			PorterDuffColorFilter filter = new PorterDuffColorFilter(
					Color.GREEN, PorterDuff.Mode.SRC_ATOP);
			d.setColorFilter(filter);
			// Atualiza variavel que permite carregar as linhas que irão compor
			// a função
			carregar = true;
			organiza();
			// Atualiza variaveis de controle
			pos1 = 0;
			pos2 = 0;
			lastbtn = 1;
		} else {

			// Atualiza variaveis de controle
			carregar = false;
			if (pos1 != 0 && pos2 != 0) {

				// Valida para aplicar a Regra Modus Ponens
				if (Teorema[pos1].getFormula().display().length() < Teorema[pos2]
						.getFormula().display().length()
						&& Teorema[pos2].getFormula().getType() == CONDITIONAL) {
					if (Teorema[pos2].getFormula().getLeft()
							.equalsTo(Teorema[pos1].getFormula()))// analisa se
																	// a
																	// regra
																	// modus
																	// pones
																	// pode
																	// ser
																	// aplicada
					{
						Teorema[++indice] = new Linha(Teorema[pos2]
								.getFormula().getRight(), " ", "MP ", qtPCRAA,
								indice);
						ajusta();
					}
				} else if (Teorema[pos1].getFormula().display().length() > Teorema[pos2]
						.getFormula().display().length()
						&& Teorema[pos1].getFormula().getType() == CONDITIONAL) {
					if (Teorema[pos1].getFormula().getLeft()
							.equalsTo(Teorema[pos2].getFormula())) {
						Teorema[++indice] = new Linha(Teorema[pos1]
								.getFormula().getRight(), " ", "MP ", qtPCRAA,
								indice);
						ajusta();
					}
				}
				alteraCor();

				organiza();
				// Nesse momento não será mais possível Refazer pois o
				// usuário
				// já realizou alguma alteração
				pos1 = 0;
				pos2 = 0;

				// Atualiza variaveis de controle
				//regraCorreta = true;
				testaRegra();
				carregar = false;
				confirma();
			}
		}
	}

	public void Regra_CJ() {
		// Executa a ação do usuário
		if (!carregar || lastbtn != 3) {
			// Altera cor do botão
			Drawable d = findViewById(R.id.btn_CJ).getBackground();
			PorterDuffColorFilter filter = new PorterDuffColorFilter(
					Color.GREEN, PorterDuff.Mode.SRC_ATOP);
			d.setColorFilter(filter);
			// Atualiza variavel que permite carregar as linhas que irão compor
			// a função
			carregar = true;
			organiza();
			// Atualiza variaveis de controle
			pos1 = 0;
			pos2 = 0;
			lastbtn = 3;
		} else {

			// Atualiza variaveis de controle
			carregar = false;

			if (pos1 != 0 && pos2 != 0) {
				Teorema[++indice] = new Linha(
						new Formula(CONJUNCTION, Teorema[pos1].getFormula(),
								Teorema[pos2].getFormula()), " ", "CJ ",
						qtPCRAA, indice);
				ajusta();

				alteraCor();
				organiza();
				// Nesse momento não será mais possível Refazer pois o
				// usuário já realizou alguma alteração

				// Atualiza variaveis de controle
				carregar = false;
				pos1 = 0;
				pos2 = 0;
				testaRegra();
				confirma();
			}
		}
	}

	public void Regra_AD() {
		// Executa a ação do usuário
		if (!carregar || lastbtn != 2) {
			// Altera cor do botão
			Drawable d = findViewById(R.id.btn_AD).getBackground();
			PorterDuffColorFilter filter = new PorterDuffColorFilter(
					Color.GREEN, PorterDuff.Mode.SRC_ATOP);
			d.setColorFilter(filter);
			// Atualiza variavel que permite carregar as linhas que irão compor
			// a função
			carregar = true;
			organiza();
			// Atualiza variaveis de controle
			pos1 = 0;
			pos2 = 0;
			lastbtn = 2;
		}
	}

	private void dialogo_AD() {
		final Dialog d = new Dialog(HeraclitoActivity.this);
		d.setContentView(R.layout.dialogo_ad);
		d.setTitle(R.string.mensagem);
		final EditText caixa = (EditText) d.findViewById(R.id.dialogocaixa);
		Button op1 = (Button) d.findViewById(R.id.bt1);
		Button op2 = (Button) d.findViewById(R.id.bt2);
		String temp = "";
		if (Teorema[pos1].getFormula().getType() != PROPOSITION
				&& Teorema[pos1].getFormula().getType() != NEGATION
				&& Teorema[pos1].getFormula().getType() != PARENTHESIS
				&& Teorema[pos1].getFormula().getType() != DISJUNCTION) {
			temp = "(" + Teorema[pos1].getFormula().display() + ")";
		} else {
			temp = Teorema[pos1].getFormula().display();
		}
		op1.setText(temp + " v");
		op2.setText("v " + temp);

		op1.setOnClickListener(new View.OnClickListener() {

			public void onClick(View v) {
				
				String temp = caixa.getText().toString();
				if (!temp.equalsIgnoreCase("")) {
					Formula f = new Formula();
					try {
						f.parse(temp);
						Teorema[++indice] = new Linha(new Formula(DISJUNCTION,
								Teorema[pos1].getFormula(), f), " ", "AD ",
								qtPCRAA, indice);
						ajusta();
						pos1 = 0;
						alteraCor();
						organiza();
						// Nesse momento não será mais possível Refazer pois
						// o usuário
						// já realizou alguma alteração

						// Atualiza variaveis de controle
						carregar = false;
						opcao = 0;
						confirma();
						regraCorreta = true;
						testaRegra();
					} catch (ScannerException e) {
					
					} catch (ParserException e) {
					
					}
				}
				d.dismiss();
			}
		});

		op2.setOnClickListener(new View.OnClickListener() {

			public void onClick(View v) {
				
				String temp = caixa.getText().toString();
				if (!temp.equalsIgnoreCase("")) {
					Formula f = new Formula();
					try {
						f.parse(temp);
						Teorema[++indice] = new Linha(new Formula(DISJUNCTION,
								f, Teorema[pos1].getFormula()), " ", "AD ",
								qtPCRAA, indice);
						ajusta();
						pos1 = 0;
						alteraCor();
						organiza();
						// Nesse momento não será mais possível Refazer pois
						// o usuário
						// já realizou alguma alteração

						// Atualiza variaveis de controle
						carregar = false;
						opcao = 0;
						confirma();
						regraCorreta = true;
						testaRegra();
					} catch (ScannerException e) {
					
					} catch (ParserException e) {
					
					}
				}
				d.dismiss();
			}
		});

		d.show();
	}

	public void Regra_DJ() {
		// Executa a ação do usuário
		if (!carregar || lastbtn != 7) {
			// Altera cor do botão
			Drawable d = findViewById(R.id.btn_DJ).getBackground();
			PorterDuffColorFilter filter = new PorterDuffColorFilter(
					Color.GREEN, PorterDuff.Mode.SRC_ATOP);
			d.setColorFilter(filter);
			// Atualiza variavel que permite carregar as linhas que irão compor
			// a função
			carregar = true;
			organiza();
			// Atualiza variaveis de controle
			pos1 = 0;
			pos2 = 0;
			pos3 = 0;
			lastbtn = 7;
		} else {

			// Atualiza variaveis de controle
			carregar = false;
			if (pos1 != 0 && pos2 != 0 && pos3 != 0) {
				Formula temp1 = null, temp2 = null, temp3 = null;

				if (Teorema[pos1].getFormula().getType() == CONDITIONAL) {
					temp1 = Teorema[pos1].getFormula();
					if (Teorema[pos2].getFormula().getType() == CONDITIONAL) {
						temp2 = Teorema[pos2].getFormula();
						if (Teorema[pos3].getFormula().getType() == DISJUNCTION) {
							temp3 = Teorema[pos3].getFormula();
						}
					} else if (Teorema[pos3].getFormula().getType() == CONDITIONAL) {
						temp2 = Teorema[pos3].getFormula();
						if (Teorema[pos2].getFormula().getType() == DISJUNCTION) {
							temp3 = Teorema[pos2].getFormula();
						}
					}
				} else if (Teorema[pos1].getFormula().getType() == DISJUNCTION) {
					temp3 = Teorema[pos1].getFormula();
					if (Teorema[pos2].getFormula().getType() == CONDITIONAL) {
						temp1 = Teorema[pos2].getFormula();
						if (Teorema[pos3].getFormula().getType() == CONDITIONAL) {
							temp2 = Teorema[pos3].getFormula();
						}
					}
				}
				if (temp1 != null && temp2 != null && temp3 != null) {
					// Valida para aplicar a Regra eliminação da disjunção

					if (temp1.getRight().equalsTo(temp2.getRight())) {
						if (temp3.getLeft().equalsTo(temp1.getLeft())
								&& temp3.getRight().equalsTo(temp2.getLeft())
								|| temp3.getRight().equalsTo(temp1.getLeft())
								&& temp3.getLeft().equalsTo(temp2.getLeft())) {
							Teorema[++indice] = new Linha(temp1.getRight(),
									" ", "-DJ ", qtPCRAA, indice);
							ajusta();
						}
					}
				}

				alteraCor();
				organiza();
				// Atualiza variaveis de controle
				carregar = false;
				pos1 = 0;
				pos2 = 0;
				pos3 = 0;
				organiza();
				testaRegra();
				confirma();
			}
		}
	}

	public void Regra_PC(String formula) {
		try {
			// Atualiza variaveis de controle
			carregar = false;
			Formula f = new Formula();
			f.parse(formula);
			f = this.eliminaParenteses(f, true);
			if (f.getType() == CONDITIONAL) {
				++qtPCRAA;
				Teorema[++indice] = new Linha(f.getLeft(), " ", "HIP-PC "
						+ f.display(), qtPCRAA, indice);

				resPCRAA[qtPCRAA - 1] = f.display();
				resPCRAA[50 - qtPCRAA] = "pc";

				ajusta();
				confirma();
				organiza();
				comunicaServidor("diag_prova", "regra aplicada");
			} else {
				// JOptionPane.showMessageDialog(null,
				// "Fórmula sem implicação.");
			}
		} catch (ScannerException ex) {
			// JOptionPane.showMessageDialog(null, "Erro na fórmula.");
		} catch (ParserException ex) {
			// JOptionPane.showMessageDialog(null, "Erro na fórmula.");
		}
	}

	public void Regra_IEQ() {
		// Executa a ação do usuário
		if (!carregar || lastbtn != 4) {
			// Altera cor do botão
			Drawable d = findViewById(R.id.btn_maisEQ).getBackground();
			PorterDuffColorFilter filter = new PorterDuffColorFilter(
					Color.GREEN, PorterDuff.Mode.SRC_ATOP);
			d.setColorFilter(filter);
			// Atualiza variavel que permite carregar as linhas que irão compor
			// a função
			carregar = true;
			organiza();
			// Atualiza variaveis de controle
			pos1 = 0;
			pos2 = 0;
			lastbtn = 4;
		} else {

			// Atualiza variaveis de controle
			carregar = false;
			if (pos1 != 0 && pos2 != 0) {

				// Valida para aplicar a Regra Introdução da equivalência
				if (Teorema[pos1].getFormula().hasLeft() && Teorema[pos2].getFormula().hasLeft())
				if (Teorema[pos1].getFormula().getLeft()
						.equalsTo(Teorema[pos2].getFormula().getRight())
						&& Teorema[pos2]
								.getFormula()
								.getLeft()
								.equalsTo(Teorema[pos1].getFormula().getRight())) {
					Formula f = new Formula(BICONDITIONAL, Teorema[pos1]
							.getFormula().getLeft(), Teorema[pos1].getFormula()
							.getRight());
					Teorema[++indice] = new Linha(f, " ", "+EQ ", qtPCRAA,
							indice);
					ajusta();
				}

				organiza();
				alteraCor();
				// Nesse momento não será mais possível Refazer pois o
				// usuário já realizou alguma alteração

				// Atualiza variaveis de controle
				carregar = false;
				pos1 = 0;
				pos2 = 0;
				testaRegra();
				confirma();
			}
		}
	}

	public void Regra_DN() {
		// Executa a ação do usuário
		if (!carregar || lastbtn != 10) {
			// Altera cor do botão
			Drawable d = findViewById(R.id.btn_DN).getBackground();
			PorterDuffColorFilter filter = new PorterDuffColorFilter(
					Color.GREEN, PorterDuff.Mode.SRC_ATOP);
			d.setColorFilter(filter);
			// Atualiza variavel que permite carregar as linhas que irão compor
			// a função
			carregar = true;
			organiza();
			// Atualiza variaveis de controle
			lastbtn = 10;
		} else {
			Formula f = Teorema[pos1].getFormula();
			if (f.getType() == NEGATION) {
				if (f.getNext().getType() == NEGATION) {
					Teorema[++indice] = new Linha(f.getNext().getNext(), " ",
							"DN ", qtPCRAA, indice);
					ajusta();
				}
			}

			// Atualiza variaveis de controle
			carregar = false;
			pos1 = 0;
			organiza();
			alteraCor();
			testaRegra();
			alteraCor();
			confirma();
		}
	}

	public void Regra_SP() {
		// Executa a ação do usuário
		if (!carregar || lastbtn != 6) {
			// Altera cor do botão
			Drawable d = findViewById(R.id.btn_SP).getBackground();
			PorterDuffColorFilter filter = new PorterDuffColorFilter(
					Color.GREEN, PorterDuff.Mode.SRC_ATOP);
			d.setColorFilter(filter);
			// Atualiza variavel que permite carregar as linhas que irão compor
			// a função
			carregar = true;
			organiza();
			// Atualiza variaveis de controle
			pos1 = 0;
			lastbtn = 6;
		} else {
			// Atualiza variaveis de controle
			carregar = false;

			if (pos1 != 0
					&& Teorema[pos1].getFormula().getType() == CONJUNCTION) {
				regraCorreta = true;
				// Valida para aplicar a Regra Introdução da equivalência
				Formula opcao1 = Teorema[pos1].getFormula().getLeft();
				Formula opcao2 = Teorema[pos1].getFormula().getRight();

				final Dialog d = new Dialog(HeraclitoActivity.this);
				d.setTitle(R.string.mensagem);
				d.setContentView(R.layout.dialogo_sp);

				final CheckBox checkbox1 = (CheckBox) d
						.findViewById(R.id.opcao1);
				final CheckBox checkbox2 = (CheckBox) d
						.findViewById(R.id.opcao2);

				checkbox1.setText(opcao1.display());
				checkbox2.setText(opcao2.display());

				Button btn_ok = (Button) d.findViewById(R.id.btn_SPok);
				Button btn_cancel = (Button) d.findViewById(R.id.btn_SPcancel);
				
				btn_ok.setOnClickListener(new View.OnClickListener() {

					public void onClick(View v) {
						
						if (checkbox1.isChecked()) {
							Teorema[++indice] = new Linha(checkbox1.getText()
									.toString(), " ", "SP ", qtPCRAA, indice);
							// jFrame1.setVisible(false);
							ajusta();

							confirma();

						}
						if (checkbox2.isChecked()) {
							Teorema[++indice] = new Linha(checkbox2.getText()
									.toString(), " ", "SP ", qtPCRAA, indice);
							//
							ajusta();

							confirma();
						}
						pos1 = 0;
						d.dismiss();
						organiza();
						alteraCor();
						confirma();
		                opcao = 0;
					}

				});
				d.show();

				btn_cancel.setOnClickListener(new View.OnClickListener() {
					
					public void onClick(View v) {
						
						d.dismiss();
					}
				});
				
				if (opcao != 0 || !regraCorreta) {
                    testaRegra();
                }
                
				 
				// organiza();
				// Nesse momento não será mais possível Refazer pois o usuário
				// já realizou alguma alteração
				// alteraCor();

				// confirma();

			}
		}
	}

	public void Regra_menosEQ() {
        //Executa a ação do usuário
        if (!carregar || lastbtn != 5) {
            Drawable d = findViewById(R.id.btn_menosEQ).getBackground();
			PorterDuffColorFilter filter = new PorterDuffColorFilter(
					Color.GREEN, PorterDuff.Mode.SRC_ATOP);
			d.setColorFilter(filter);
            //Atualiza variavel que permite carregar as linhas que irão compor a função
            carregar = true;
            //Atualizar as variaveis do teorema antes de manupila-los(remove as <<<<< caso o usuário tenha trocado de regra antes de finalizar a anterior)
            Teorema[pos1].unselect();
            Teorema[pos2].unselect();
            organiza();
            //Atualiza variaveis de controle
            pos1 = 0;
            pos2 = 0;
            lastbtn = 5;
        } else {

            //Atualiza variaveis de controle
            carregar = false;
        
        if (pos1 != 0 && Teorema[pos1].getFormula().getType() == BICONDITIONAL) {
            //Valida para aplicar a Regra Introdução da equivalência
        	regraCorreta = true;
            Formula opcao1 = new Formula(CONDITIONAL, Teorema[pos1].getFormula().getLeft(), Teorema[pos1].getFormula().getRight());
            Formula opcao2 = new Formula(CONDITIONAL, Teorema[pos1].getFormula().getRight(), Teorema[pos1].getFormula().getLeft());
            
            final Dialog d = new Dialog(HeraclitoActivity.this);
			d.setContentView(R.layout.dialogo_sp);
			d.setTitle(R.string.mensagem);
        	
        	final CheckBox checkbox1 = (CheckBox) d.findViewById(R.id.opcao1);
            final CheckBox checkbox2 = (CheckBox) d.findViewById(R.id.opcao2);
            
            checkbox1.setText(opcao1.display());
            checkbox2.setText(opcao2.display());
            
            Button btn_ok = (Button) d.findViewById(R.id.btn_SPok);
            Button btn_cancel = (Button) d.findViewById(R.id.btn_SPcancel);
            
            btn_ok.setOnClickListener(new View.OnClickListener() {
				
				public void onClick(View v) {
					
					if (checkbox1.isChecked()) {
						Teorema[++indice] = new Linha(checkbox1.getText().toString(), " ", "-EQ ", qtPCRAA, indice);
		                ajusta();
		                confirma();
					}
					if (checkbox2.isChecked()) {
						Teorema[++indice] = new Linha(checkbox2.getText().toString(), " ", "-EQ ", qtPCRAA, indice);
		                ajusta();
		                confirma();
		                
					}
					pos1 = 0;
					d.dismiss();
					organiza();
					
					if (opcao != 0 || !regraCorreta) {
						testaRegra();
					}
					confirma();
					opcao = 0;
				}
			});
            d.show();
            
            btn_cancel.setOnClickListener(new View.OnClickListener() {
				
				public void onClick(View v) {
					
					d.dismiss();
				}
			});
            
            
					
			//            organiza();
            //Nesse momento não será mais possível Refazer pois o usuário já realizou alguma alteração

            //confirma();
        }
    }
        
	}
	
	public void Regra_MT() {
		// Executa a aÃ§Ã£o do usuÃ¡rio
		if (!carregar || lastbtn != 11) {
			// Altera cor do botÃ£o
			Drawable d = findViewById(R.id.btn_MT).getBackground();
			PorterDuffColorFilter filter = new PorterDuffColorFilter(
					Color.GREEN, PorterDuff.Mode.SRC_ATOP);
			d.setColorFilter(filter);
			// Atualiza variavel que permite carregar as linhas que irÃ£o compor
			// a funÃ§Ã£o
			carregar = true;
			organiza();
			// Atualiza variaveis de controle
			pos1 = 0;
			pos2 = 0;
			lastbtn = 11;
		} else {

			// Atualiza variaveis de controle
			carregar = false;
			if (pos1 != 0 && pos2 != 0) {

				// Valida para aplicar a Regra Modus Tollens
				if (Teorema[pos1].getFormula().display().length() < Teorema[pos2]
						.getFormula().display().length()
						&& Teorema[pos2].getFormula().getType() == CONDITIONAL) {
					if (Teorema[pos2].getFormula().getRight().getType() == NEGATION) {
						if (Teorema[pos2].getFormula().getRight().getNext()
								.equalsTo(Teorema[pos1].getFormula()))// analisa
																		// se a
																		// regra
																		// modus
																		// pones
																		// pode
																		// ser
																		// aplicada
						{
							Teorema[++indice] = new Linha(new Formula(NEGATION,
									Teorema[pos2].getFormula().getLeft()), " ",
									"MT ", qtPCRAA, indice);
							ajusta();
						}
					} else if (Teorema[pos1].getFormula().getType() == NEGATION) {
						if (Teorema[pos2].getFormula().getRight()
								.equalsTo(Teorema[pos1].getFormula().getNext()))// analisa
																				// se
																				// a
																				// regra
																				// modus
																				// pones
																				// pode
																				// ser
																				// aplicada
						{
							Teorema[++indice] = new Linha(new Formula(NEGATION,
									Teorema[pos2].getFormula().getLeft()), " ",
									"MT ", qtPCRAA, indice);
							ajusta();
						}
					}
				} else if (Teorema[pos1].getFormula().display().length() > Teorema[pos2]
						.getFormula().display().length()
						&& Teorema[pos1].getFormula().getType() == CONDITIONAL) {
					if (Teorema[pos1].getFormula().getRight().getType() == NEGATION) {
						if (Teorema[pos1].getFormula().getRight().getNext()
								.equalsTo(Teorema[pos2].getFormula()))// analisa
																		// se a
																		// regra
																		// modus
																		// pones
																		// pode
																		// ser
																		// aplicada
						{
							Teorema[++indice] = new Linha(new Formula(NEGATION,
									Teorema[pos1].getFormula().getLeft()), " ",
									"MT ", qtPCRAA, indice);
							ajusta();
						}
					} else if (Teorema[pos2].getFormula().getType() == NEGATION) {
						if (Teorema[pos1].getFormula().getRight()
								.equalsTo(Teorema[pos2].getFormula().getNext()))// analisa
																				// se
																				// a
																				// regra
																				// modus
																				// pones
																				// pode
																				// ser
																				// aplicada
						{
							Teorema[++indice] = new Linha(new Formula(NEGATION,
									Teorema[pos1].getFormula().getLeft()), " ",
									"MT ", qtPCRAA, indice);
							ajusta();
						}
					}
				}

				organiza();
				// Nesse momento nÃ£o serÃ¡ mais possÃ­vel Refazer pois o
				// usuÃ¡rio jÃ¡ realizou alguma alteraÃ§Ã£o
				pos1 = 0;
				pos2 = 0;
				alteraCor();

				// Atualiza variaveis de controle
				carregar = false;
				organiza();
				testaRegra();
				confirma();
			}
		}
	}

	public void Regra_SD() {
		// Executa a aÃ§Ã£o do usuÃ¡rio
		if (!carregar || lastbtn != 13) {
			// Altera cor do botÃ£o
			Drawable d = findViewById(R.id.btn_SD).getBackground();
			PorterDuffColorFilter filter = new PorterDuffColorFilter(
					Color.GREEN, PorterDuff.Mode.SRC_ATOP);
			d.setColorFilter(filter);
			// Atualiza variavel que permite carregar as linhas que irÃ£o compor
			// a funÃ§Ã£o
			carregar = true;
			organiza();
			// Atualiza variaveis de controle
			pos1 = 0;
			pos2 = 0;
			lastbtn = 13;
		} else {

			// Atualiza variaveis de controle
			carregar = false;
			if (pos1 != 0 && pos2 != 0) {

				Formula f;
				// Valida para aplicar a Regra Silogismo HipotÃ©tico
				if (Teorema[pos1].getFormula().getType() == DISJUNCTION) {
					if (Teorema[pos2].getFormula().getType() == NEGATION) {
						f = Teorema[pos2].getFormula().getNext();
					} else {
						f = new Formula(NEGATION, Teorema[pos2].getFormula());
					}
					if (f.equalsTo(Teorema[pos1].getFormula().getRight())) {
						Teorema[++indice] = new Linha(Teorema[pos1]
								.getFormula().getLeft(), " ", "SD ", qtPCRAA,
								indice);
					}
					if (f.equalsTo(Teorema[pos1].getFormula().getLeft())) {
						Teorema[++indice] = new Linha(Teorema[pos1]
								.getFormula().getRight(), " ", "SD ", qtPCRAA,
								indice);
					}
				} else if (Teorema[pos2].getFormula().getType() == DISJUNCTION) {
					if (Teorema[pos1].getFormula().getType() == NEGATION) {
						f = Teorema[pos1].getFormula().getNext();
					} else {
						f = new Formula(NEGATION, Teorema[pos1].getFormula());
					}
					if (f.equalsTo(Teorema[pos2].getFormula().getRight())) {
						Teorema[++indice] = new Linha(Teorema[pos2]
								.getFormula().getLeft(), " ", "SD ", qtPCRAA,
								indice);
					}
					if (f.equalsTo(Teorema[pos2].getFormula().getLeft())) {
						Teorema[++indice] = new Linha(Teorema[pos2]
								.getFormula().getRight(), " ", "SD ", qtPCRAA,
								indice);
					}
				}

				organiza();
				alteraCor();
				// Nesse momento nÃ£o serÃ¡ mais possÃ­vel Refazer pois o
				// usuÃ¡rio jÃ¡ realizou alguma alteraÃ§Ã£o
				pos1 = 0;
				pos2 = 0;
				testaRegra();
				// Atualiza variaveis de controle
				carregar = false;
				confirma();
			}
		}
	}

	public void Regra_SH() {
		// Executa a aÃ§Ã£o do usuÃ¡rio
		if (!carregar || lastbtn != 12) {
			// Altera cor do botÃ£o
			Drawable d = findViewById(R.id.btn_SH).getBackground();
			PorterDuffColorFilter filter = new PorterDuffColorFilter(
					Color.GREEN, PorterDuff.Mode.SRC_ATOP);
			d.setColorFilter(filter);
			// Atualiza variavel que permite carregar as linhas que irÃ£o compor
			// a funÃ§Ã£o
			carregar = true;
			organiza();
			// Atualiza variaveis de controle
			pos1 = 0;
			pos2 = 0;
			lastbtn = 12;
		} else {

			// Atualiza variaveis de controle
			carregar = false;
			if (pos1 != 0 && pos2 != 0) {

				// Valida para aplicar a Regra Silogismo HipotÃ©tico
				if (Teorema[pos1].getFormula().getType() == CONDITIONAL
						&& Teorema[pos2].getFormula().getType() == CONDITIONAL) {
					if (Teorema[pos1].getFormula().getRight()
							.equalsTo(Teorema[pos2].getFormula().getLeft())) {
						Teorema[++indice] = new Linha(new Formula(CONDITIONAL,
								Teorema[pos1].getFormula().getLeft(),
								Teorema[pos2].getFormula().getRight()), " ",
								"SH ", qtPCRAA, indice);
					} else if (Teorema[pos2].getFormula().getRight()
							.equalsTo(Teorema[pos1].getFormula().getLeft())) {
						Teorema[++indice] = new Linha(new Formula(CONDITIONAL,
								Teorema[pos2].getFormula().getLeft(),
								Teorema[pos1].getFormula().getRight()), " ",
								"SH ", qtPCRAA, indice);
					}
				}

				organiza();
				alteraCor();
				// Nesse momento nÃ£o serÃ¡ mais possÃ­vel Refazer pois o
				// usuÃ¡rio jÃ¡ realizou alguma alteraÃ§Ã£o
				pos1 = 0;
				pos2 = 0;

				// Atualiza variaveis de controle
				carregar = false;
				organiza();
				testaRegra();
				confirma();
			}
		}
	}

	public void Regra_DC() {
		// Executa a aÃ§Ã£o do usuÃ¡rio
		if (!carregar || lastbtn != 15) {
			// Altera cor do botÃ£o
			Drawable d = findViewById(R.id.btn_DC).getBackground();
			PorterDuffColorFilter filter = new PorterDuffColorFilter(
					Color.GREEN, PorterDuff.Mode.SRC_ATOP);
			d.setColorFilter(filter);
			// Atualiza variavel que permite carregar as linhas que irÃ£o compor
			// a funÃ§Ã£o
			carregar = true;
			organiza();
			// Atualiza variaveis de controle
			pos1 = 0;
			pos2 = 0;
			pos3 = 0;
			lastbtn = 15;
		} else {

			// Atualiza variaveis de controle
			carregar = false;
			if (pos1 != 0 && pos2 != 0 && pos3 != 0) {
				Formula temp1 = null, temp2 = null, temp3 = null;

				if (Teorema[pos1].getFormula().getType() == CONDITIONAL) {
					temp1 = Teorema[pos1].getFormula();
					if (Teorema[pos2].getFormula().getType() == CONDITIONAL) {
						temp2 = Teorema[pos2].getFormula();
						if (Teorema[pos3].getFormula().getType() == DISJUNCTION) {
							temp3 = Teorema[pos3].getFormula();
						}
					} else if (Teorema[pos3].getFormula().getType() == CONDITIONAL) {
						temp2 = Teorema[pos3].getFormula();
						if (Teorema[pos2].getFormula().getType() == DISJUNCTION) {
							temp3 = Teorema[pos2].getFormula();
						}
					}
				} else if (Teorema[pos1].getFormula().getType() == DISJUNCTION) {
					temp3 = Teorema[pos1].getFormula();
					if (Teorema[pos2].getFormula().getType() == CONDITIONAL) {
						temp1 = Teorema[pos2].getFormula();
						if (Teorema[pos3].getFormula().getType() == CONDITIONAL) {
							temp2 = Teorema[pos3].getFormula();
						}
					}
				}
				if (temp1 != null && temp2 != null && temp3 != null) {
					// Valida para aplicar a Regra eliminaÃ§Ã£o da disjunÃ§Ã£o

					if (temp3.getRight().equalsTo(temp2.getLeft())) {
						if (temp3.getLeft().equalsTo(temp1.getLeft())) {
							Formula f = new Formula(DISJUNCTION,
									temp1.getRight(), temp2.getRight());
							Teorema[++indice] = new Linha(f, " ", "DC ",
									qtPCRAA, indice);
						}
					} else {
						if (temp3.getRight().equalsTo(temp1.getLeft())) {
							if (temp3.getLeft().equalsTo(temp2.getLeft())) {
								Formula f = new Formula(DISJUNCTION,
										temp1.getRight(), temp2.getRight());
								Teorema[++indice] = new Linha(f, " ", "DC ",
										qtPCRAA, indice);
							}
						}
					}
				}

				organiza();
				alteraCor();
				// Atualiza variaveis de controle
				carregar = false;
				pos1 = 0;
				pos2 = 0;
				pos3 = 0;
				testaRegra();
				confirma();
			}

		}
	}

	public void Regra_EXP() {
		// Executa a aÃ§Ã£o do usuÃ¡rio
		if (!carregar || lastbtn != 16) {
			// Altera cor do botÃ£o
			Drawable d = findViewById(R.id.btn_EXP).getBackground();
			PorterDuffColorFilter filter = new PorterDuffColorFilter(
					Color.GREEN, PorterDuff.Mode.SRC_ATOP);
			d.setColorFilter(filter);
			// Atualiza variavel que permite carregar as linhas que irÃ£o compor
			// a funÃ§Ã£o
			carregar = true;
			organiza();
			// Atualiza variaveis de controle
			pos1 = 0;
			lastbtn = 16;
		} else {

			// Atualiza variaveis de controle
			carregar = false;
			if (pos1 != 0) {
				if (Teorema[pos1].getFormula().getType() == CONDITIONAL) {
					Formula f = Teorema[pos1].getFormula().getLeft();
					while (f.getType() == PARENTHESIS) {
						f = f.getNext();
					}
					if (f.getType() == CONJUNCTION) {
						Formula aux = new Formula(CONDITIONAL, f.getLeft(),
								Teorema[pos1].getFormula().getRight());
						aux = new Formula(CONDITIONAL, f.getRight(), aux);
						Teorema[++indice] = new Linha(aux, " ", "EXP ",
								qtPCRAA, indice);
					}
				}
				organiza();
				alteraCor();
				// Nesse momento nÃ£o serÃ¡ mais possÃ­vel Refazer pois o
				// usuÃ¡rio jÃ¡ realizou alguma alteraÃ§Ã£o
				pos1 = 0;

				// Atualiza variaveis de controle
				carregar = false;
				organiza();
				testaRegra();
				confirma();
			}
		}
	}

	public void Regra_INC() {
		// Executa a aÃ§Ã£o do usuÃ¡rio
		if (!carregar || lastbtn != 14) {
			// Altera cor do botÃ£o
			Drawable d = findViewById(R.id.btn_INC).getBackground();
			PorterDuffColorFilter filter = new PorterDuffColorFilter(
					Color.GREEN, PorterDuff.Mode.SRC_ATOP);
			d.setColorFilter(filter);
			// Atualiza variavel que permite carregar as linhas que irÃ£o compor
			// a funÃ§Ã£o
			carregar = true;
			organiza();
			// Atualiza variaveis de controle
			pos1 = 0;
			pos2 = 0;
			lastbtn = 14;
		} else {
			// Atualiza variaveis de controle
			carregar = false;
			if (pos1 != 0 && pos2 != 0) {

				// Valida para aplicar a Regra InconsistÃªncia
				if (Teorema[pos1].getFormula().getType() == NEGATION) {
					if (Teorema[pos1].getFormula().getNext()
							.equalsTo(Teorema[pos2].getFormula())) {
						dialogoINC();
						regraCorreta = true;
					}
				} else if (Teorema[pos2].getFormula().getType() == NEGATION) {
					if (Teorema[pos2].getFormula().getNext()
							.equalsTo(Teorema[pos1].getFormula())) {
						dialogoINC();
						regraCorreta = true;
					}
				}

				organiza();
				alteraCor();
				// Nesse momento nÃ£o serÃ¡ mais possÃ­vel Refazer pois o
				// usuÃ¡rio jÃ¡ realizou alguma alteraÃ§Ã£o
				
				// Atualiza variaveis de controle
				carregar = false;
				organiza();
				testaRegra();
				confirma();
			}
		}
	}

	private void dialogoINC() {

		final Dialog d = new Dialog(HeraclitoActivity.this);
		d.setContentView(R.layout.dialogo);
		d.setTitle(R.string.mensagem);

		Button ok = (Button) d.findViewById(R.id.btok);
		Button bcan = (Button) d.findViewById(R.id.bcancel);
		final EditText caixa = (EditText) d.findViewById(R.id.dialogocaixa);
		TextView tv = (TextView) d.findViewById(R.id.textView1);
		tv.setText(getString(R.string.regra_inc) + "\n" + getString(R.string.regra_inc_exemplo));

		ok.setOnClickListener(new View.OnClickListener() {

			public void onClick(View v) {
				
				String temp = caixa.getText().toString();
				if (!temp.equalsIgnoreCase(""))
					aplicaINC(temp);
				d.dismiss();
			}
		});

		bcan.setOnClickListener(new View.OnClickListener() {

			public void onClick(View v) {
				

				d.dismiss();
			}
		});

		d.show();
	}

	private void aplicaINC(String formula) {
		
		try {
			Formula f = new Formula();
			f.parse(formula);
			f = this.eliminaParenteses(f, true);
			Teorema[++indice] = new Linha(f, " ", "INC ", qtPCRAA, indice);

			ajusta();
			regraCorreta = false;
			
			organiza();

			comunicaServidor("diag_prova", "regra aplicada");
			alteraCor();
			confirma();
		} catch (ScannerException ex) {
			// JOptionPane.showMessageDialog(null, "Erro na fÃ³rmula");
		} catch (ParserException ex) {
			// JOptionPane.showMessageDialog(null, "Erro na fÃ³rmula");
		}
		pos1 = 0;
		pos2 = 0;
	}

	
	
	private void organiza() {
		
		
		
		String lista[] = new String[indice + 1];
		
		if (Teorema[0] == null) {
			return;
		}
		
		for (int x = 0; x < lista.length; ++x) {
			lista[x] = Teorema[x].toString();
		}
		// teoremalist.setAdapter(new
		// ArrayAdapter<String>(HeraclitoActivity.this,
		// android.R.layout.simple_list_item_1, lista));
		selectedAdapter = new SelectedAdapter(this, 0, lista);
		selectedAdapter.setNotifyOnChange(false);
		teoremalist.setAdapter(selectedAdapter);

	//lista.size	
		//teoremalist.smoothScrollToPosition(selectedAdapter.getCount() - 1);
		
		ScrollerRunnable scroll = new ScrollerRunnable(teoremalist);
		scroll.start(selectedAdapter.getCount() - 1);
		
		
		indiceoriginal = indice;
		
		TeoremaAux = Teorema.clone();
		//indiceoriginal = indice;

		 // Atualiza a lista auxiliar do teorema
	}
	
	private String getDate() {
		String date = new String();
		
		if (Calendar.getInstance().get(Calendar.HOUR_OF_DAY) < 10) {
			date += "0";
		}
		date += Calendar.getInstance().get(Calendar.HOUR_OF_DAY) + ":";
		
		if (Calendar.getInstance().get(Calendar.MINUTE) < 10) {
			date += "0";
		}
		date += Calendar.getInstance().get(Calendar.MINUTE) + ":";
		
		if (Calendar.getInstance().get(Calendar.SECOND) < 10) {
			date += "0";
		}
		date += Calendar.getInstance().get(Calendar.SECOND);
		return date;
	}
	
	private void escreveParaUsuario(String msg) {
		msgAgent.add(this.getDate() + " - " + msg);

		msgAgent.trimToSize();
		
		final String[] aux = msgAgent.toArray(new String[msgAgent.size()]);
		
		/**
		Object[] conversaoArray = msgAgent.toArray();
		final String aux[] = new String[conversaoArray.length];
		
		for (int i = 0; i < conversaoArray.length; i++) {
			aux[i] = conversaoArray[i].toString();
		}**/
	
		//runOnUiThread
		//final String auxFinal = aux;
		
		runOnUiThread(new Runnable() {
		    public void run() {
		        // runs on UI thread

				selectedAdapterAgent = new SelectedAdapterAgent(getBaseContext(), 0, aux);
				selectedAdapterAgent.setNotifyOnChange(true);
				agentCommList.setAdapter(selectedAdapterAgent);
				
				ScrollerRunnable scroll2 = new ScrollerRunnable(agentCommList);
				scroll2.start(selectedAdapterAgent.getCount() - 1);
				
				selectedAdapterAgent.setSelectedPosition(selectedAdapterAgent.getCount() - 1);
				//agentCommList.smoothScrollToPosition(selectedAdapterAgent.getCount() - 1);
				
			   }
		});
			
	}
	
	
	
	private void atualizaLista() {
		String lista[] = new String[indice + 1];
		
		if (Teorema[0] == null) {
			return;
		}
		
		for (int x = 0; x < lista.length; ++x) {
			lista[x] = Teorema[x].toString();
		}
		// teoremalist.setAdapter(new
		// ArrayAdapter<String>(HeraclitoActivity.this,
		// android.R.layout.simple_list_item_1, lista));
		selectedAdapter = new SelectedAdapter(this, 0, lista);
		selectedAdapter.setNotifyOnChange(true);
		teoremalist.setAdapter(selectedAdapter);
	}

	public Formula eliminaParenteses(Formula f, boolean root) {
		if (root) {
			while (f.getType() == PARENTHESIS) {
				f = f.getNext();
			}
		}

		if (f.getType() == NEGATION) {
			f.setNext(eliminaParenteses(f.getNext(), false));
		}
		if (f.getType() == PARENTHESIS) {
			if (f.getNext().getType() == PARENTHESIS) {
				f = f.getNext();
				f = eliminaParenteses(f, false);
			}
			f.setNext(eliminaParenteses(f.getNext(), false));

		}
		if (f.getLeft() != null) {
			if (f.getLeft().getType() == PARENTHESIS
					&& (f.getLeft().getNext().getType() == PROPOSITION
							|| f.getLeft().getNext().getType() == NEGATION || f
							.getLeft().getNext().getType() == PARENTHESIS)) {
				f.setLeft(f.getLeft().getNext());
				f = eliminaParenteses(f, false);
			}
			f.setLeft(eliminaParenteses(f.getLeft(), false));
		}
		if (f.getRight() != null) {
			if (f.getRight().getType() == PARENTHESIS
					&& (f.getRight().getNext().getType() == PROPOSITION
							|| f.getRight().getNext().getType() == NEGATION || f
							.getRight().getNext().getType() == PARENTHESIS)) {
				f.setRight(f.getRight().getNext());
				f = eliminaParenteses(f, false);
			}
			f.setRight(eliminaParenteses(f.getRight(), false));
		}
		return f;
	}

	public void Iniciar() {
		Limpar();
		String aux[];
		resPCRAA = new String[50];
		String argumento;
		
		if (nivel.equalsIgnoreCase("Adicionar Argumento")) {
			argumento = adicionar_argumento.getText().toString();
		} else {
			argumento = sp1.getSelectedItem().toString();
		}
		//argumento = adicionar_argumento.getText().toString();
		
		
		
		
		if (argumento != null && !argumento.isEmpty() && argumento.contains("|-")) {

			// teoremalist.clear();

			Teorema[0] = new Teorema("Argumento: "
					+ argumento); // Carrega o teorema do
															// usuário

			aux = argumento.split(",");// Separa o
																// teorema para
																// exibir as
																// hipóteses

			total_hipoteses = aux.length; // Total de hipoteses. Controle para o
											// desfazer

			if (aux[0].startsWith("|-")) {
				--total_hipoteses;
			}
			
			hipoteses = new Formula[total_hipoteses + 1];

			try {
				// Copia o teorema como hipótese
				if (argumento.indexOf("|-") != 0) {
					for (int i = 0; i < aux.length; i++) {
						 if ((i + 1) != aux.length) {
	                            hipoteses[i] = new Formula();
	                            hipoteses[i].parse(aux[i]);
	                            hipoteses[i] = eliminaParenteses(hipoteses[i], true);
	                        } else {
	                            hipoteses[i] = new Formula();
	                            hipoteses[i].parse(aux[i].substring(0, aux[i].indexOf("|-")));
	                            hipoteses[i] = eliminaParenteses(hipoteses[i], true);
	                        }
					}
					indice = 0; // Atualizar variavel auxiliar de controle
				} else {
					indice = 0;
					// jButton13.setEnabled(false);
				}
					/**Formula f = new Formula();
					for (int i = 0; i < aux.length; i++) {
						if ((i + 1) != aux.length) {
							f.parse(aux[i]);
							hipoteses[i] = new Linha(f.display(), "", "HIP", 0,
									i);
							hipoteses[i].setFormula(eliminaParenteses(
									hipoteses[i].getFormula(), true));
						} else {
							f.parse(aux[i].substring(0, aux[i].indexOf("|-")));
							hipoteses[i] = new Linha(f.display(), "", "HIP", 0,
									i);
							hipoteses[i].setFormula(eliminaParenteses(
									hipoteses[i].getFormula(), true));
						}
					}
					indice = 0; // Atualizar variavel auxiliar de controle
				} else {
					indice = 0;
					// jButton13.setEnabled(false);
					// jButton11.setEnabled(false);
				}
				// txtTeorema.setText(""); //Limpa o campo do teorema
				// txtTeorema.setEditable(false); //Bloqueia edição do campo
				**/
				formataArgumento();
				TeoremaAux = Teorema.clone(); // Atualiza a lista auxiliar do
												// teorema

				indiceoriginal = aux.length; // Atualizar variavel auxiliar de
												// controle
				
				organiza(); // Carrega lista com os novos dados do Teorema
				//mostraHip();
				habilitaBotoesInterface();
				separador.setVisibility(View.INVISIBLE);

			} catch (Exception ex) {
				Utils.createDialogHelper(this, R.string.aviso, R.string.erro_argumento, true);		
			}
			
		}
		 comunicaServidor("novo_argumento", "Novo Argumento");      
	}
	
	public void adicionaHip(String aux, TextSwitcher mensagemHip) {
		Formula f = new Formula();
		boolean temp = false; //assinala se a hip�tese est� correta.
		
		if (aux != null && !aux.equalsIgnoreCase("")) {
            try {
                f.parse(aux);
                for (int x = 0; x < hipoteses.length; ++x) {
                    if (hipoteses[x] != null) {
                        if (f.equalsTo(hipoteses[x])) {
                            temp = true;
                            Teorema[++indice] = new Linha(f, "", "HIP ", 0, indice);
                            for (int y = x; y < hipoteses.length - 1; ++y) {
                                hipoteses[y] = hipoteses[y + 1];
                            }
                        }
                    }
                }
                if (!temp) {
                    this.escreveParaUsuario(getString(R.string.hipotese_incorreta));
                    comunicaServidor("diag_hipotese", "erro hipotese");
                } else {
                    this.escreveParaUsuario(getString(R.string.hipotese_sucesso));
                    comunicaServidor("diag_hipotese", "hipotese informada");
                }
                //organiza();
                if (hipoteses[0] == null) {
                    this.escreveParaUsuario(getString(R.string.hipotese_inseridas));
                    
                    // this.setBotoes(true, false, true);
                }

                organiza();
            } catch (ScannerException ex) {
                mensagemHip.setText(getString(R.string.formula_erro));
            	//JOptionPane.showMessageDialog(null, "Erro na f�rmula.");
            } catch (ParserException ex) {
            	mensagemHip.setText(getString(R.string.formula_erro));
            	//JOptionPane.showMessageDialog(null, "Erro na f�rmula.");
            }
        }

				
	}

	public void mostraHip() {
		if (hipoteses[0] != null) {
			for (int x = 0; x < hipoteses.length; ++x) {
				if (hipoteses[x] != null) {
					Teorema[++indice] = new Linha(hipoteses[x],
							"", "HIP", 0, indice);
				}
			}
			for (int y = 0; y < hipoteses.length - 1; ++y) {
				hipoteses[y] = null;
			}
			// this.setBotoes(true);
		}
		organiza();
	}

	private void alteraCor() {
		if (ultimoBotao != 0) {
			Drawable d = findViewById(ultimoBotao).getBackground();
			findViewById(ultimoBotao).invalidateDrawable(d);
			d.clearColorFilter();
		}
	}

	private void ajusta() {// ajusta Teorema[indice] com os nº das linhas e com
							// a regra utilizada
		regraCorreta = true;
		Teorema[indice].setFormula(eliminaParenteses(
				Teorema[indice].getFormula(), true));
		if (Teorema[indice].getPos().equals(" ")) {
			if (pos1 == 0) {
				Teorema[indice].setPos("");
			} else if (pos2 == 0) {
				Teorema[indice].setPos("" + pos1);
			} else if (pos3 == 0) {
				if (pos1 < pos2) {
					Teorema[indice].setPos(pos1 + "," + pos2);
				} else {
					Teorema[indice].setPos(pos2 + "," + pos1);
				}
			} else if (pos1 < pos2) {
				if (pos1 < pos3) {
					if (pos2 < pos3) {
						Teorema[indice].setPos(pos1 + "," + pos2 + "," + pos3);
					} else {
						Teorema[indice].setPos(pos1 + "," + pos3 + "," + pos2);
					}
				} else {
					Teorema[indice].setPos(pos3 + "," + pos1 + "," + pos2);
				}
			} else if (pos2 < pos3) {
				if (pos1 < pos3) {
					Teorema[indice].setPos(pos2 + "," + pos1 + "," + pos3);
				} else {
					Teorema[indice].setPos(pos2 + "," + pos3 + "," + pos1);
				}
			} else {
				Teorema[indice].setPos(pos3 + "," + pos2 + "," + pos1);
			}
		}
	}

	private void confirma() {
		if (qtPCRAA > 0) {
			if (resPCRAA[50 - qtPCRAA].equals("pc")) {
				confirmaPC();
			} else {
				confirmaRAA();
			}
		}
		// testa se a prova está completa
		if (qtPCRAA == 0) {
			if (Teorema[indice].getFormula().equalsTo(Teorema[0].getFormula())) {
				if (resolucao == null) {
				  Utils.createDialogHelper(this, R.string.mensagem, R.string.prova_sucesso, true);	
				} else {
					//vR.string.resolucao_provador
					Builder dialog = Utils.createDialogHelper(this, R.string.mensagem, R.string.resolucao_provador, false);

					dialog.setPositiveButton(R.string.sim,
							new DialogInterface.OnClickListener() {

								public void onClick(DialogInterface dialog,
										int which) {
									separador.setVisibility(0);
									selectedAdapterProvador = new SelectedAdapter(
											getApplicationContext(), 0,
											resolucao);
									provadorlist
											.setAdapter(selectedAdapterProvador);
								}
							});

					dialog.setNegativeButton(R.string.nao,
							new DialogInterface.OnClickListener() {

								public void onClick(DialogInterface dialog,
										int which) {
									// TODO Auto-generated method stub
									dialog.dismiss();
								}
							});

					dialog.show();
				}
				/**
				//Toast.makeText(getApplicationContext(), "Prova completada!", Toast.LENGTH_LONG).show();// lstTeorema.setEnabled(false);
				Builder = Utils.createDialogHelper( dialog = new Builder = Utils.createDialogHelper((HeraclitoActivity.this);
	            dialog.setMessage(getString(R.string.prova_sucesso));
	            dialog.setNeutralButton("OK", null);
	            dialog.setTitle(R.string.mensagem);
	            dialog.show();	     */       
			}
		}
	}

	private void confirmaPC() {
		try {
			// testa se a regra PC pode ser finalizada
			Formula f = new Formula();
			f.parse(resPCRAA[qtPCRAA - 1]);
			if (Teorema[indice].getFormula().equalsTo(f.getRight())) {
				--qtPCRAA;
				Teorema[++indice] = new Linha(resPCRAA[qtPCRAA], " ", "PC ",
						qtPCRAA, indice);

				ajusta();
				confirma();
				organiza();
				comunicaServidor("diag_prova", "regra aplicada");
				terminaPCRAA();
			}
		} catch (ScannerException ex) {
			// Logger.getLogger(Edicao.class.getName()).log(Level.SEVERE, null,
			// ex);
		} catch (ParserException ex) {
			// Logger.getLogger(Edicao.class.getName()).log(Level.SEVERE, null,
			// ex);
		}
	}

	private void confirmaRAA() {// testa se há um absurdo
		Formula temp = Teorema[indice].getFormula();
		if (temp.getType() == CONJUNCTION) {
			try {
				Formula f = new Formula();
				f.parse(resPCRAA[qtPCRAA - 1]);
				if (temp.getLeft().getType() == NEGATION) {
					if (temp.getLeft().getNext().equalsTo(temp.getRight())) {
						--qtPCRAA;
						if (f.getType() != PROPOSITION
								&& f.getType() != PARENTHESIS
								&& f.getType() != NEGATION) {
							Teorema[++indice] = new Linha("~("
									+ resPCRAA[qtPCRAA] + ")", " ", "RAA ",
									qtPCRAA, indice);
						} else {
							Teorema[++indice] = new Linha("~"
									+ resPCRAA[qtPCRAA], " ", "RAA ", qtPCRAA,
									indice);
						}
						organiza();
						terminaPCRAA();
						if (qtPCRAA > 0) {
							confirma();
						}
					}
				} else if (temp.getRight().getType() == NEGATION) {
					if (temp.getRight().getNext().equalsTo(temp.getLeft())) {
						--qtPCRAA;
						if (f.getType() != PROPOSITION
								&& f.getType() != PARENTHESIS
								&& f.getType() != NEGATION) {
							Teorema[++indice] = new Linha("~("
									+ resPCRAA[qtPCRAA] + ")", " ", "RAA ",
									qtPCRAA, indice);
						} else {
							Teorema[++indice] = new Linha("~"
									+ resPCRAA[qtPCRAA], " ", "RAA ", qtPCRAA,
									indice);
						}
						organiza();
						terminaPCRAA();
						if (qtPCRAA > 0) {
							confirma();
						}
					}
				}
				ajusta();
                comunicaServidor("diag_prova", "regra aplicada");
			} catch (ScannerException ex) {
				// Logger.getLogger(Edicao.class.getName()).log(Level.SEVERE,
				// null, ex);
			} catch (ParserException ex) {
				// Logger.getLogger(Edicao.class.getName()).log(Level.SEVERE,
				// null, ex);
			}
		}
	}

	public void Limpar() {

		// Zera todas as variaveis de controle dos teoremas
		Teorema = new Linha[100];
		TeoremaAux = Teorema.clone();
		msgAgent = new ArrayList<String>();
		qtPCRAA = 0;
		// Limpa as variaveis de tela
		String[] a = new String[0];
		teoremalist.setAdapter(new ArrayAdapter<String>(HeraclitoActivity.this,
				android.R.layout.simple_list_item_1, a));
		agentCommList.setAdapter(new ArrayAdapter<String>(HeraclitoActivity.this,
				android.R.layout.simple_list_item_1, a));
		provadorlist.setAdapter(new ArrayAdapter<String>(HeraclitoActivity.this,
				android.R.layout.simple_list_item_1, a));
		// txtTeorema.setEditable(true);
		// this.setBotoes(false);
		// Atualiza as variaveis de controle e cores dos botões
		pos1 = 0;
		pos2 = 0;
		pos3 = 0;
		indice = 0;
		carregar = false;
		alteraCor();
	}

	private void terminaPCRAA() {
		int aux;
		for (int x = indice -1; x > 0; --x) {
			aux = Teorema[x].getQtPCRAA();
			if (aux == qtPCRAA + 1) {
				Teorema[x].setUnusable();
			} else if (aux == qtPCRAA) {
				return;
			}
		}
	}
	
	private void desfazer() {
		if (indice > total_hipoteses) { //Se não for o início do teorema pode Desfazer

            indice--; //Atualizar variavel auxiliar de controle

            for (int i = 0; i <= indice; i++) { //Carrega o teorema principal com os dados do teorema auxiliar, com base no indice auxiliar
                Teorema[i] = TeoremaAux[i];
            }

            Teorema[indice + 1] = null; //Limpa a última posição do teorema

            qtPCRAA = Teorema[indice].getQtPCRAA();
            atualizaLista();
            //lstTeorema.clearSelection(); //Limpa lista
            //lstTeorema.setListData(Teorema); //Carrega lista com os novos dados do Teorema
            //lstTeorema.setEnabled(true);
		}
	}
	
	private void refazer() {
		if (indiceoriginal > indice) { //Verifica se pode ser refeito com base nas últimas alterações
			//Toast.makeText(getBaseContext(), "dpois do if", Toast.LENGTH_SHORT).show();
            indice++;  //Atualizar variavel auxiliar de controle

            for (int i = 0; i <= indice; i++) { //Carrega o teorema principal com os dados do teorema auxiliar, com base no indice auxiliar
                Teorema[i] = TeoremaAux[i];
            }

            qtPCRAA = Teorema[indice].getQtPCRAA();
            atualizaLista();
            //lstTeorema.clearSelection(); //Limpa lista
            //lstTeorema.setListData(Teorema); //Carrega lista com os novos dados do Teorema
        }

	}
	
	private void leArquivoArgumentos() {
		InputStream argumentos = null;

		ArrayList<String> lista = new ArrayList<String>();
		try {
			// TODO Workaround gambiarra reversa
			if (sp2_selecionar.getSelectedItem().toString().equals(getString(R.string.nivel_basico))) {
				nivel = "Basico";
			} else if (sp2_selecionar.getSelectedItem().toString().equals(getString(R.string.nivel_intermediario))) {
				nivel = "Intermediario";
			} else if (sp2_selecionar.getSelectedItem().toString().equals(getString(R.string.nivel_avancado))) {
				nivel = "Avancado";
			} else if (sp2_selecionar.getSelectedItem().toString().equals(getString(R.string.nivel_exercicios))) {
				nivel = "Lista_de_exercicio";
			}
			
			//nivel = sp2_selecionar.getSelectedItem().toString();
			
			
			argumentos = getBaseContext().getAssets()
					.open("Exercicios" + System.getProperty("file.separator")
							+ nivel);
			InputStreamReader isr = new InputStreamReader(argumentos);
			BufferedReader bf = new BufferedReader(isr);

			lista.add(bf.readLine());
			while (lista.get(lista.size() - 1) != null) {
				lista.add(bf.readLine());
			}
			bf.close();

		} catch (IOException e1) {
			e1.printStackTrace();
		}

		lista.remove(lista.size() - 1);

		sp1.setAdapter(new ArrayAdapter<String>(HeraclitoActivity.this,
				android.R.layout.simple_list_item_1, lista));
		
		System.out.println("debug");
		// TODO Workaround
		//View nivel_basico = sp1.getChildAt(0);
		
		//TextView nivel_basico = (TextView) sp2_selecionar.getChildAt(0);
		//nivel_basico.setText(R.string.nivel_basico);
		/**TextView nivel_intermediario = (TextView) sp1.getChildAt(1);
		nivel_intermediario.setText(R.string.nivel_intermediario);
		TextView nivel_avancado = (TextView) sp1.getChildAt(2);
		nivel_avancado.setText(R.string.nivel_avancado);
		TextView nivel_argumento = (TextView) sp1.getChildAt(3);
		nivel_argumento.setText(R.string.nivel_argumento);**/
		
	}
	
	private void formataArgumento() {
        argumentoFormatado = "[";
        for (int x = 0; x < total_hipoteses; ++x) {
            argumentoFormatado += hipoteses[x].display() + ", ";
        }
        if (total_hipoteses > 0) {
            argumentoFormatado = argumentoFormatado.substring(0, argumentoFormatado.length() - 2);
        }
        argumentoFormatado += " ] :-- " + Teorema[0].getFormula().display() + ".";
    }
	
	
	private void comunicaServidor(String tipo, String tipo2) {
		if (MainActivity.usuario != null) {
            String msg = tipo + "(" + '"' + this.nivel + '"' + "," + '"' + this.argumentoFormatado + '"' + "," + '"';
            if (indice > 0) {
                msg += this.formataProva();
            }
            msg += '"' + "," + '"' + tipo2 + '"' + "," + MainActivity.usuario + ")";
            
            //Toast.makeText(getApplicationContext(), msg, Toast.LENGTH_LONG).show();
            
            new sendMessageAsync().execute(msg);
           
        }
	}
	
    private String formataProva() {
        String prova = '"' + "";
       
        for (int x = 1; x < indice + 1; ++x) {
            prova += Teorema[x].formata() + "\n";
        }
       
        prova = prova.substring(0, prova.lastIndexOf("\n")) + '"';
        return prova;
    }

	private void testaRegra() {
	        if (!regraCorreta) {
	            //this.testaQtErros();
	            escreveParaUsuario("Regra incorreta");
	            comunicaServidor("diag_prova", "erro regra-" + regras[lastbtn - 1]);
	            
	        } else {
	           // qtErrosRegras[lastbtn - 1] = 0;
	            regraCorreta = false;
	            escreveParaUsuario("Regra aplicada com sucesso ");
	            comunicaServidor("diag_prova", "regra aplicada");
	            
	        }
	}
	
	public void formataResolucaoProvador(String msg) {
        String aux[] = msg.replace('"' + "", "").split(";");
        String aux2[] = new String[5];
        int aux3 = 0;
        String msgAux;
        resolucao = new String[aux.length + 1];
        resolucao[0] = "Resolução do provador:";
        for (int x = 0; x < aux.length; ++x) {
            aux2[0] = aux[x].substring(0, 6);
            aux2[1] = aux[x].substring(6, 10);
            aux2[2] = aux[x].substring(10, 35);
            aux2[3] = aux[x].substring(35, 45);
            aux2[4] = aux[x].substring(45);
            msgAux = aux2[0].substring(0, aux[x].indexOf("."));
            int tam = 4 - msgAux.length();
            for (int y = 0; y < tam; ++y) {
                msgAux += " ";
            }
            aux3 = Integer.parseInt(aux2[1].substring(0, aux2[1].indexOf(".")));
            for (int z = 0; z < aux3; ++z) {
                msgAux += "| ";
            }
            msgAux += aux2[2];
            tam = 39 - msgAux.length();
            for (int y = 0; y < tam; ++y) {
                msgAux += " ";
            }
            msgAux += aux2[3].trim() + " " + aux2[4].replace("[", "").replace("]", "");
            resolucao[x + 1] = msgAux.replace(".", "").replace("'", "").toUpperCase().replaceAll("V", "v");
        }
    }
	
	public class sendMessageAsync extends AsyncTask<String, String, String>{
		fipaMessage fipaMessage;

		public sendMessageAsync() {

		}
		
		@Override
		protected String doInBackground(String... params) {
			
			fipaMessage = new fipaMessage();//cria uma nova mensagem fipa
	        fipaMessage.setUserId(MainActivity.usuario);
	        fipaMessage.setPerformative(7);
	        fipaMessage.setAgentTo("perfilaluno");//nome do agente que receberá a mensagem
	        fipaMessage.setContent(params[0]);//mensagem com a informção desejada
			
			//preciso mandar para o agente o tipo AsyncHandler mas � muita m�o
			
			//request2.addProperty("asyncHandler", "AsyncHandler<SendMessageToAgentResponse> asyncHandler"); //d� para enganar passando String
			request2.addProperty("fipaMessage", fipaMessage);
			
			SoapSerializationEnvelope envelope = new SoapSerializationEnvelope(SoapEnvelope.VER11);
			envelope.setOutputSoapObject(request2);
			
			HttpTransportSE transport = new HttpTransportSE(URL); //objeto de conexao com ws
			String resposta = null;
			
			try {
				transport.call(SOAP_ACTION2, envelope);
				
				SoapPrimitive agentResponse = (SoapPrimitive) envelope.getResponse();
			
				/**
				SoapObject propriedades = (SoapObject) envelope.bodyIn;
				
				int count = propriedades.getPropertyCount();
				
				for (int i = 0; i < count; i++) {
					resposta += propriedades.getProperty(i); 
				}**/
				
				
				//s� retorna timeout
				
				//Response<SendMessageToAgentResponse> r = (Response<SendMessageToAgentResponse>) envelope.getResponse();
				//resposta = r.get().getReturn();
				
				
				resposta = agentResponse.toString();
				
			} catch (IOException e) {
				
			} catch (XmlPullParserException e) {
		
			} catch (NullPointerException e) {
				
			}
			
			//publishProgress();
			//Toast.makeText(mContext, resposta, Toast.LENGTH_LONG).show();
			
			return resposta;
			}
		
		private void testMessageFromAgent(String msg) {
		    if (msg == null) {
		    	Log.d("TestMessageAgent: ", "NULL");
		    	return;
		    }
			
			if (msg.equals("TIMEOUT")) {
		    	return;
		    }
		    
		    if (msg.contains("ok")) {
		    	return;
		    }
			//String aux = msg.substring(msg.indexOf("(") + 1, msg.lastIndexOf(","));
			
		    String aux = msg.substring(msg.indexOf('(') + 1, msg.lastIndexOf(','));
			//String aux = msg.substring(msg.indexOf("(") +1);
            //String aux = msg;
		    
		    // Workaround
		    aux = corrigeAcentos(aux);
		    
		    if (msg.contains("verifica_ajuda") || msg.contains("informar") || msg.contains("diag_hipotese")) {
            	escreveParaUsuario(aux);
            } else if (msg.contains("sugerir_exemplo")) {
            	ofereceExemplos(aux);
            } else if (msg.contains("diag_prova")) {
                if (aux.contains("prejudicial")) {
                    prejudicial(aux);
                } else {
                    escreveParaUsuario(aux);
                }
            } else if (msg.contains("solic_ajuda")) {
            	prejudicial(aux);
                //JOptionPane.showConfirmDialog(null, aux, "", JOptionPane.YES_NO_OPTION); 
            } else if(msg.contains("novo_argumento")){
                formataResolucaoProvador(msg.substring(msg.indexOf(".,") + 2, msg.lastIndexOf(",")));
            }
            
        }
		
		
		
		private void prejudicial(String msg) {
			final String aux = msg;
			
			
			
			runOnUiThread(new Runnable() {
			    public void run() {
			        // runs on UI thread
			    	
			    	
					Builder dialog = Utils.createDialogHelper(HeraclitoActivity.this, R.string.aviso, aux, false);
		            
		            if (aux.contains("solic_ajuda")) {
		            	dialog.setNeutralButton("OK", new DialogInterface.OnClickListener() {
							
							public void onClick(DialogInterface dialog, int which) {
								
															}
						});
		            	
					} else {
						dialog.setNeutralButton("OK", null);
					}
		            		            
		            dialog.show();
			    }
			});
			
	    }
		
		private String corrigeAcentos(String msg) {
			if (msg.contains("voce")) {
				msg.replace("voce", getString(R.string.workaround_voce));
			}
			
			else if (msg.contains("Parabens")) {
				msg = getString(R.string.workaround_parabens);
			} 
			
			else if (msg.contains("pois nao contribui para a resolucao")) {
				msg = getString(R.string.workaround_redundante);
			}
			
			else if (msg.contains("prejudicial")) {
				msg = getString(R.string.workaround_prejudicial);
			}
			
			else if (msg.contains("ainda")) {
				msg = getString(R.string.workaround_ainda);
			}
			
			else if (msg.contains("ja informaste")) {
				msg = getString(R.string.workaround_ja);
			}
			
			else if (msg.contains("Gostaria de analisar um exemplo?")) {
				msg = getString(R.string.workaround_aplicou);
			}
			
			return msg;
			
		}
		
		@Override
		protected void onPostExecute(String result) {
			//Toast t = Toast.makeText(getApplicationContext(), result, Toast.LENGTH_LONG);
			//t.setGravity(Gravity.TOP, 20, 300);
			//t.show();
			 testMessageFromAgent(result);
		}
		
		}
		
	
	
	public class Login extends AsyncTask<String, String, String> {
		ProgressBar progressBar;
		Context mContext;
		Dialog loginDialog;
		TextSwitcher mensagemLogin;
		TextView mensagemUsuarioLogado;
		String mensagemUsuarioUser;
		
		public Login(Context mContext, ProgressBar mProgressBar, Dialog loginDialog, TextSwitcher mensagemLogin, TextView mensagemUsuarioLogado) {
			this.mContext = mContext;
			this.progressBar = mProgressBar;
			this.loginDialog = loginDialog;
			this.mensagemLogin = mensagemLogin;
			this.mensagemUsuarioLogado = mensagemUsuarioLogado;
		}
		
		@Override 
		protected void onPreExecute() {

			AlphaAnimation fadeIn;
			fadeIn = new AlphaAnimation(0,1); //fade out animation from 1 (fully visible) to 0 (transparent)
			fadeIn.setDuration(150); //set duration in mill seconds
			//fadeIn.setFillAfter(true);
			progressBar.startAnimation(fadeIn);
			
			TextView loginTexto = (TextView) mensagemLogin.getChildAt(0);
			loginTexto.setTextColor(Color.BLACK);
						
			TextView loginTexto2 = (TextView) mensagemLogin.getChildAt(1);
			loginTexto2.setTextColor(Color.BLACK);
			
			progressBar.setVisibility(View.VISIBLE);
			mensagemLogin.setText(getString(R.string.autenticando) + "...");
		}
		
		@Override
		protected String doInBackground(String... params) {
			mensagemUsuarioUser = params[0];
			
			request.addProperty("userId", params[0]);
			request.addProperty("password", params[1]);
			request.addProperty("localHost", "");
			
			SoapSerializationEnvelope envelope = new SoapSerializationEnvelope(SoapEnvelope.VER11);
			envelope.setOutputSoapObject(request);
			
			HttpTransportSE transport = new HttpTransportSE(URL); //objeto de conexao com ws
			String resposta = new String();
			
			try {
				transport.call(SOAP_ACTION, envelope);
				
				Object response = envelope.getResponse();
				
				if (response != null) {
					if (response instanceof SoapPrimitive) {
						SoapPrimitive respostaAgente = (SoapPrimitive) response;
						resposta = respostaAgente.toString();
					} else if (response instanceof SoapObject) {
						//SoapObject answerAgent = (SoapObject) response;
						
						resposta = getString(R.string.login_invalido);
						/**
						for (int i = 0; i < answerAgent.getPropertyCount(); i++) {
							resposta += answerAgent.getProperty(i).toString();
						}**/
						
					}
					//mensagemLogin.setCurrentText(resposta);
					//Toast.makeText(getBaseContext(), response.toString(), Toast.LENGTH_LONG).show();
				}
				
			} catch (IOException e) {
				
				e.printStackTrace();
			} catch (XmlPullParserException e) {
				
				e.printStackTrace();
			}
			
			publishProgress();
			//Toast.makeText(mContext, resposta, Toast.LENGTH_LONG).show();
			return resposta;
		}
		
		@Override
		protected void onPostExecute(String result) {
	        //espera();
			
			//progressBar.setVisibility(View.GONE);
			if (result != null) {
				
				//Toast.makeText(mContext, result, Toast.LENGTH_LONG).show();
				if (!result.contains("logado")) {
					mensagemLogin.setText(result);
				}
				
				AlphaAnimation fadeOut;
				fadeOut = new AlphaAnimation(1,0); //fade out animation from 1 (fully visible) to 0 (transparent)
				fadeOut.setDuration(3100); //set duration in mill seconds
				fadeOut.setFillAfter(true);
				progressBar.startAnimation(fadeOut);
				
				
				if (result.contains("Erro") || result.contains("Digite")) {
					return;
				} else {
					espera();
					
					//loginDialog.dismiss();
				}
				
				
			} else {
				mensagemLogin.setText(getString(R.string.impossivel_login));
				//Toast.makeText(mContext, "não foi possível fazer login", Toast.LENGTH_LONG).show();
			}
			
			
			
			
			//Toast.makeText(mContext, result, Toast.LENGTH_SHORT).show();
		}
		
		@Override 
		protected void onProgressUpdate(String... values) {
			
			//progressBar.setProgress(0x1);
			//Toast.makeText(mContext, values[0], Toast.LENGTH_SHORT).show();
		}
		
		public void espera() {
			final Handler handler = new Handler(); 
		       
			Timer t = new Timer(); 
	        t.schedule(new TimerTask() { 
	                public void run() { 
	                        handler.post(new Runnable() { 
	                                public void run() { 
	                                	loginDialog.dismiss();
	                                	//mensagemUsuarioLogado.setText(getString(R.string.usuario_logado) + mensagemUsuarioUser);
	                                } 
	                        }); 
	                } 
	        }, 2500); 
	        
		}
		
	
	}

	public void Salvar(String filePath) {
        File f = new File(filePath); //atribui a f o arquivo selecionado
        if (f != null)//confere se o arquivo selecionado n�o � null
        {
            try {
                f = ajustaFile(f);
                FileOutputStream fos = new FileOutputStream(f);
                ObjectOutputStream os = new ObjectOutputStream(fos);
                os.writeObject(qtPCRAA);
                os.writeObject(resPCRAA);
                os.writeObject(Teorema);
                os.close();

                FileWriter fr = new FileWriter(ajustaFiletxt(f));
                PrintWriter out = new PrintWriter(fr);
                //salva as informa��es no arquivo
                for (int x = 0; x <= indice; ++x) {
                    out.println(Teorema[x]);
                }
                out.close();
            } catch (IOException e) {
               Log.e("MARCEL", e.toString());
            	//Toast.makeText(HeraclitoActivity.class., "Erro ao salvar o arquivo", Toast.LENGTH_LONG).show();
            }
        }
    }
	
	  private File ajustaFile(File f) {//ajusta o aruivo selecionado para que termine com .her
	        String aux = f.getAbsolutePath();
	        if (aux.length() < 4) {
	            aux += ".her";
	        } else if (!aux.substring(aux.length() - 4).equals(".her")) {
	            aux += ".her";
	        }
	        return new File(aux);
	    }

	    private File ajustaFiletxt(File f) {//ajusta o aruivo selecionado para que termine com .txt
	        String aux = f.getAbsolutePath();
	        aux = aux.substring(0, aux.length() - 4) + ".txt";
	        return new File(aux);
	    }
	    
		public void Abrir(String filePath) {
	        //confere se o arquivo selecionado n�o � null
	            try {
	            	File f = new File(filePath);
	            	if (f != null) {
	            		FileInputStream fos = new FileInputStream(f);
	                    ObjectInputStream os = new ObjectInputStream(fos);
	                    qtPCRAA = (Integer) os.readObject();
	                    resPCRAA = (String[]) os.readObject();
	                    Teorema = (Linha[]) os.readObject();
	                    if (Teorema[0].toString() == null) {
	                        Limpar();
	                    } else {
	                        for (indice = 0; Teorema[indice] != null; ++indice);
	                        --indice;
	                        organiza();
	                        if (indice > 0) {
	                            String aux[] = Teorema[0].toString().split(",");
	                            aux[0] = aux[0].substring(aux[0].indexOf(":") + 1);
	                            if (aux.length > indice) {
	                                boolean hipAdicionada = false;
	                                int qtHip = 0;
	                                total_hipoteses = aux.length;
	                                hipoteses = new Formula[total_hipoteses];
	                                try {
	                                    Formula f1;
	                                    for (int x = 0; x < total_hipoteses; ++x) {
	                                        if (!aux[x].contains("|-")) {
	                                            f1 = new Formula();
	                                            f1.parse(aux[x]);
	                                        } else {
	                                            f1 = new Formula();
	                                            f1.parse(aux[x].substring(0, aux[x].indexOf("|-")));
	                                        }
	                                        for (int y = 1; y < indice + 1; ++y) {
	                                            if (f1.equalsTo(Teorema[y].getFormula())) {
	                                                hipAdicionada = true;
	                                            }
	                                        }
	                                        if (!hipAdicionada) {
	                                            hipoteses[qtHip++] = f1;
	                                        } else {
	                                            hipAdicionada = false;
	                                        }
	                                    }
	                                } catch (ScannerException e) {
	                                	Toast.makeText(HeraclitoActivity.this, e.toString(), Toast.LENGTH_LONG).show();
	                                	Log.e(e.toString(), e.toString());
	                                } catch (ParserException ex) {
	                                	Toast.makeText(HeraclitoActivity.this, ex.toString(), Toast.LENGTH_LONG).show();
	                                	Log.e(ex.toString(), ex.toString());
	                                }
	                            }
	                      }
	                        	if (indice > 0) {
	                        		if (Teorema[indice].getFormula().equalsTo(Teorema[0].getFormula())) {
		                            	habilitaBotoesInterface();
		                            }
	                        	}
	                            
	                        }
	                    }
	            	
	            	habilitaBotoesInterface();
	            		
	                } catch (IOException e) {
	                	Toast.makeText(HeraclitoActivity.this, e.toString(), Toast.LENGTH_LONG).show();
	                	Log.e("MARCEL!", e.toString());
	                } catch (ClassNotFoundException ex) {
	                	Log.e("MARCEL!", ex.toString());
	                	Toast.makeText(HeraclitoActivity.this, ex.toString(), Toast.LENGTH_LONG).show();
	                }
		}
	
		public void ofereceExemplos(String mensagemDoAgente) {
			Builder dialog = Utils.createDialogHelper(this, R.string.mensagem, mensagemDoAgente, false);

			dialog.setPositiveButton(R.string.sim,
					new DialogInterface.OnClickListener() {

						public void onClick(DialogInterface dialog,
								int which) {
							SelecaoExemplos(null);
						}
					});

			dialog.setNegativeButton(R.string.nao,
					new DialogInterface.OnClickListener() {

						public void onClick(DialogInterface dialog,
								int which) {
							// TODO Auto-generated method stub
							dialog.dismiss();
						}
					});

			dialog.show();
		}
		
}
